Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
100a0e7c
Commit
100a0e7c
authored
Apr 22, 2015
by
MARCHE Claude
Browse files
removed useless usage of String.set in why3doc
parent
cf45aa11
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/why3doc/doc_def.ml
View file @
100a0e7c
...
...
@@ -30,9 +30,6 @@ let output_file fname =
in
base
^
".html"
type
url
=
string
type
anchor
=
string
let
tag_allowed_char
=
let
tbl
=
Array
.
make
256
false
in
let
s
=
"-_:"
in
(* '.' is removed so as to be used as an escape char below *)
...
...
@@ -43,51 +40,34 @@ let tag_allowed_char =
span
'
0
'
'
9
'
;
fun
c
->
tbl
.
(
Char
.
code
c
)
let
tag_escape
s
=
let
len
=
ref
0
in
String
.
iter
(
fun
c
->
if
tag_allowed_char
c
then
incr
len
else
len
:=
!
len
+
3
)
s
;
let
len'
=
!
len
in
let
len
=
String
.
length
s
in
if
len
=
len'
then
s
else
begin
let
hex
=
"0123456789ABCDEF"
in
let
t
=
String
.
create
len'
in
let
j
=
ref
0
in
for
i
=
0
to
len
-
1
do
let
c
=
s
.
[
i
]
in
if
tag_allowed_char
c
then
begin
t
.
[
!
j
]
<-
c
;
incr
j
end
else
begin
let
pp_tag_escape
=
let
hex
=
"0123456789ABCDEF"
in
fun
fmt
s
->
String
.
iter
(
fun
c
->
if
tag_allowed_char
c
then
Format
.
fprintf
fmt
"%c"
c
else
let
c
=
Char
.
code
c
in
t
.
[
!
j
]
<-
'.'
;
t
.
[
!
j
+
1
]
<-
hex
.
[
c
/
16
];
t
.
[
!
j
+
2
]
<-
hex
.
[
c
mod
16
];
j
:=
!
j
+
3
end
done
;
t
end
Format
.
fprintf
fmt
".%c%c"
hex
.
[
c
/
16
]
hex
.
[
c
mod
16
])
s
let
make_tag
s
l
=
tag_escape
s
^
"_"
^
string_of_int
l
let
pp_tag
fmt
s
l
=
Format
.
fprintf
fmt
"%a_%d"
pp_tag_escape
s
l
let
local_files
=
Hashtbl
.
create
17
let
add_local_file
fn
=
Hashtbl
.
add
local_files
(
Filename
.
chop_extension
fn
)
()
let
is_local_file
=
Hashtbl
.
mem
local_files
let
make_url
fn
=
let
url
=
fn
^
".html"
in
match
!
stdlib_url
with
|
Some
www
when
not
(
is_local_file
fn
)
->
www
^
"/"
^
url
|
_
->
url
let
pp_url
fmt
lp
=
if
lp
<>
[]
then
let
fn
=
String
.
concat
"."
lp
in
match
!
stdlib_url
with
|
Some
www
when
not
(
is_local_file
fn
)
->
Format
.
fprintf
fmt
"%s/%s.html"
www
fn
|
_
->
Format
.
fprintf
fmt
"%s.html"
fn
let
anchor
id
=
match
id
.
id_loc
with
let
pp_
anchor
fmt
id
=
match
id
.
id_loc
with
|
None
->
raise
Not_found
|
Some
loc
->
let
_
,
l
,
_
,
_
=
Loc
.
get
loc
in
make_tag
id
.
id_string
l
|
Some
loc
->
let
_
,
l
,
_
,
_
=
Loc
.
get
loc
in
pp_tag
fmt
id
.
id_string
l
let
locate
id
=
let
pp_
locate
fmt
id
=
let
lp
,
_
,
_
=
try
Mlw_module
.
restore_path
id
with
Not_found
->
Theory
.
restore_path
id
in
let
url
=
if
lp
=
[]
then
""
else
make_url
(
String
.
concat
"."
lp
)
in
url
^
"#"
^
anchor
id
Format
.
fprintf
fmt
"%a#%a"
pp_url
lp
pp_anchor
id
src/why3doc/doc_def.mli
View file @
100a0e7c
...
...
@@ -21,12 +21,7 @@ val set_stdlib_url: string -> unit
val
output_file
:
string
->
string
type
anchor
=
string
val
pp_anchor
:
Format
.
formatter
->
ident
->
unit
val
anchor
:
ident
->
string
type
url
=
string
val
locate
:
ident
->
url
val
pp_locate
:
Format
.
formatter
->
ident
->
unit
(* or raises [Not_found] *)
src/why3doc/doc_lexer.mll
View file @
100a0e7c
...
...
@@ -96,11 +96,9 @@
try
match
Glob
.
find
loc
with
|
id
,
Glob
.
Def
->
let
t
=
Doc_def
.
anchor
id
in
fprintf
fmt
"<a name=
\"
%s
\"
>%s</a>"
t
s
fprintf
fmt
"<a name=
\"
%a
\"
>%s</a>"
Doc_def
.
pp_anchor
id
s
|
id
,
Glob
.
Use
->
let
url
=
Doc_def
.
locate
id
in
fprintf
fmt
"<a href=
\"
%s
\"
>%s</a>"
url
s
fprintf
fmt
"<a href=
\"
%a
\"
>%s</a>"
Doc_def
.
pp_locate
id
s
with
Not_found
->
(* otherwise, just print it *)
pp_print_string
fmt
s
...
...
@@ -339,4 +337,3 @@ Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3doc.opt"
End:
*)
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment