\n\n"
+ end
let trailer () =
if !header_trailer && !footer_file_spec then
let cin = open_in !footer_file in
- try
- while true do
+ try
+ while true do
let s = input_line cin in
- printf "%s\n" s
- done
+ printf "%s\n" s
+ done
with End_of_file -> close_in cin
else
begin
if !index && (get_module false) <> "Index" then
printf "
\n\n\n\n
\n\n\n"
+ printf "This page has been generated by ";
+ printf "coqdoc\n" Coq_config.wwwcoq;
+ printf "
\n\n
\n\n\n"
end
let start_module () =
@@ -595,12 +595,12 @@ module Html = struct
fun s ->
Buffer.clear buff;
for i = 0 to String.length s - 1 do
- match s.[i] with
- | '<' -> Buffer.add_string buff "<"
- | '>' -> Buffer.add_string buff ">"
- | '&' -> Buffer.add_string buff "&"
+ match s.[i] with
+ | '<' -> Buffer.add_string buff "<"
+ | '>' -> Buffer.add_string buff ">"
+ | '&' -> Buffer.add_string buff "&"
| '\"' -> Buffer.add_string buff """
- | c -> Buffer.add_char buff c
+ | c -> Buffer.add_char buff c
done;
Buffer.contents buff
@@ -628,16 +628,16 @@ module Html = struct
let start_quote () = char '"'
let stop_quote () = start_quote ()
- let start_verbatim inline =
+ let start_verbatim inline =
if inline then printf ""
else printf "
"
- let stop_verbatim inline =
- if inline then printf "
"
+ let stop_verbatim inline =
+ if inline then printf ""
else printf "\n"
- let url addr name =
- printf "%s" addr
+ let url addr name =
+ printf "%s" addr
(match name with
| Some n -> n
| None -> addr)
@@ -645,29 +645,29 @@ module Html = struct
let ident_ref m fid typ s =
match find_module m with
| Local ->
- printf "" m (sanitize_name fid);
- printf "%s" typ s
+ printf "" m (sanitize_name fid);
+ printf "%s" typ s
| External m when !externals ->
- printf "" m (sanitize_name fid);
- printf "%s" typ s
+ printf "" m (sanitize_name fid);
+ printf "%s" typ s
| External _ | Unknown ->
- printf "%s" typ s
+ printf "%s" typ s
let reference s r =
match r with
| Def (fullid,ty) ->
- printf "" (sanitize_name fullid);
- printf "%s" (type_name ty) s
+ printf "" (sanitize_name fullid);
+ printf "%s" (type_name ty) s
| Ref (m,fullid,ty) ->
- ident_ref m fullid (type_name ty) s
+ ident_ref m fullid (type_name ty) s
let output_sublexer_string doescape issymbchar tag s =
let s = if doescape then escaped s else s in
match tag with
| Some ref -> reference s ref
| None ->
- if issymbchar then output_string s
- else printf "%s" s
+ if issymbchar then output_string s
+ else printf "%s" s
let sublexer c loc =
let tag =
@@ -686,7 +686,7 @@ module Html = struct
let translate s =
match Tokens.translate s with Some s -> s | None -> escaped s
- let keyword s loc =
+ let keyword s loc =
printf "%s" (translate s)
let ident s loc =
@@ -697,14 +697,14 @@ module Html = struct
reference (translate s) (Index.find (get_module false) loc)
with Not_found ->
if is_tactic s then
- printf "%s" (translate s)
+ printf "%s" (translate s)
else if is_keyword s then
printf "%s" (translate s)
else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then
try reference (translate s) (Index.find_string s)
- with Not_found -> Tokens.output_tagged_ident_string s
+ with Not_found -> Tokens.output_tagged_ident_string s
else
- Tokens.output_tagged_ident_string s
+ Tokens.output_tagged_ident_string s
let proofbox () = printf "☐"
@@ -748,7 +748,7 @@ module Html = struct
let end_code () = end_coq (); start_doc ()
- let start_inline_coq () =
+ let start_inline_coq () =
if !inline_notmono then printf ""
else printf ""
@@ -758,7 +758,7 @@ module Html = struct
let end_inline_coq_block () = end_inline_coq ()
- let paragraph () = printf "\n
\n\n"
+ let paragraph () = printf "\n
\n\n"
(* inference rules *)
let inf_rule assumptions (_,_,midnm) conclusions =
@@ -766,12 +766,12 @@ module Html = struct
in a row with " "s. We do this to the assumptions so that
people can put multiple rules on a line with nice formatting *)
let replace_spaces str =
- let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in
+ let rec copy a n = match n with 0 -> [] | n -> (a :: copy a (n - 1)) in
let results = Str.full_split (Str.regexp "[' '][' '][' ']+") str in
let strs = List.map (fun r -> match r with
| Str.Text s -> [s]
- | Str.Delim s ->
- copy " " (String.length s))
+ | Str.Delim s ->
+ copy " " (String.length s))
results
in
String.concat "" (List.concat strs)
@@ -782,7 +782,7 @@ module Html = struct
let end_assumption () =
(printf "
\n";
printf "\n") in
- let rec print_assumptions hyps =
+ let rec print_assumptions hyps =
match hyps with
| [] -> start_assumption " "
| [(_,hyp)] -> start_assumption hyp
@@ -793,7 +793,7 @@ module Html = struct
print_assumptions assumptions;
printf "
\n";
@@ -827,9 +827,9 @@ module Html = struct
let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
printf "
%s %s
\n" idx c (display_letter c) cat;
List.iter
- (fun (id,(text,link,t)) ->
- let id' = prepare_entry id t in
- printf "%s %s \n" link id' text) l;
+ (fun (id,(text,link,t)) ->
+ let id' = prepare_entry id t in
+ printf "%s %s \n" link id' text) l;
printf "
"
end
@@ -840,35 +840,35 @@ module Html = struct
let format_global_index =
Index.map
(fun s (m,t) ->
- if t = Library then
+ if t = Library then
let ln = !lib_name in
if ln <> "" then
"[" ^ String.lowercase_ascii ln ^ "]", m ^ ".html", t
else
- "[library]", m ^ ".html", t
- else
- sprintf "[%s, in %s]" (type_name t) m m ,
- sprintf "%s.html#%s" m (sanitize_name s), t)
+ "[library]", m ^ ".html", t
+ else
+ sprintf "[%s, in %s]" (type_name t) m m ,
+ sprintf "%s.html#%s" m (sanitize_name s), t)
let format_bytype_index = function
| Library, idx ->
- Index.map (fun id m -> "", m ^ ".html", Library) idx
+ Index.map (fun id m -> "", m ^ ".html", Library) idx
| (t,idx) ->
- Index.map
- (fun s m ->
- let text = sprintf "[in %s]" m m in
- (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
+ Index.map
+ (fun s m ->
+ let text = sprintf "[in %s]" m m in
+ (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
(* Impression de la table d'index *)
let print_index_table_item i =
printf "
\n
%s Index
\n" (String.capitalize_ascii i.idx_name);
List.iter
(fun (c,l) ->
- if l <> [] then
- printf "
\n" (index_ref i c)
+ (display_letter c)
+ else
+ printf "
%s
\n" (display_letter c))
i.idx_entries;
let n = i.idx_size in
printf "
(%d %s)
\n" n (if n > 1 then "entries" else "entry");
@@ -896,45 +896,45 @@ module Html = struct
let make_multi_index () =
let all_index =
let glob,bt = Index.all_entries () in
- (format_global_index glob) ::
- (List.map format_bytype_index bt) in
+ (format_global_index glob) ::
+ (List.map format_bytype_index bt) in
let print_table () = print_index_table all_index in
List.iter (make_one_multi_index print_table) all_index
let make_index () =
let all_index =
let glob,bt = Index.all_entries () in
- (format_global_index glob) ::
- (List.map format_bytype_index bt) in
+ (format_global_index glob) ::
+ (List.map format_bytype_index bt) in
let print_table () = print_index_table all_index in
let print_one_index i =
if i.idx_size > 0 then begin
printf "\n
%s Index
\n" (String.capitalize_ascii i.idx_name);
- all_letters i
+ all_letters i
end
in
set_module "Index" None;
if !title <> "" then printf "
%s
\n" !title;
print_table ();
if not (!multi_index) then
- begin
- List.iter print_one_index all_index;
- printf ""; print_table ()
- end
+ begin
+ List.iter print_one_index all_index;
+ printf ""; print_table ()
+ end
let make_toc () =
- let ln = !lib_name in
+ let ln = !lib_name in
let make_toc_entry = function
| Toc_library (m,sub) ->
- stop_item ();
- let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
+ stop_item ();
+ let ms = match sub with | None -> m | Some s -> m ^ ": " ^ s in
if ln = "" then
- printf "
\n";
Queue.iter make_toc_entry toc_q;
@@ -990,7 +990,7 @@ module TeXmacs = struct
let start_verbatim inline = in_doc := true; printf "<\\verbatim>"
let stop_verbatim inline = in_doc := false; printf ""
- let url addr name =
+ let url addr name =
printf "%s<\\footnote><\\url>%s" addr
(match name with
| None -> ""
@@ -1126,7 +1126,7 @@ module Raw = struct
let start_verbatim inline = ()
let stop_verbatim inline = ()
- let url addr name =
+ let url addr name =
match name with
| Some n -> printf "%s (%s)" n addr
| None -> printf "%s" addr
@@ -1285,7 +1285,7 @@ let verbatim_char inline =
select (if inline then Latex.char else output_char) Html.char TeXmacs.char Raw.char
let hard_verbatim_char = output_char
-let url =
+let url =
select Latex.url Html.url TeXmacs.url Raw.url
let start_quote =
@@ -1293,15 +1293,15 @@ let start_quote =
let stop_quote =
select Latex.stop_quote Html.stop_quote TeXmacs.stop_quote Raw.stop_quote
-let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
+let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions =
start_verbatim false;
- let dumb_line =
+ let dumb_line =
function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln);
char '\n')
- in
+ in
(List.iter dumb_line assumptions;
- dumb_line (midsp, midln ^ (match midnm with
- | Some s -> " " ^ s
+ dumb_line (midsp, midln ^ (match midnm with
+ | Some s -> " " ^ s
| None -> ""));
List.iter dumb_line conclusions);
stop_verbatim false
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index ceed67fff2..62da608348 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -98,7 +98,7 @@ val url : string -> string option -> unit
something smart we can just format the rule verbatim like the user did
*)
val inf_rule : (int * string) list
- -> (int * string * (string option))
+ -> (int * string * (string option))
-> (int * string) list
-> unit
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 5adc18e1a0..0e7071425f 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -104,45 +104,45 @@ let buffer_char is_symbolchar ctag c =
restart_buffering ()
| Buffering (was_symbolchar,tag,translated,tt) ->
if tag <> ctag then
- (* A strong tag comes from Coq; if different Coq tags *)
- (* hence, we don't try to see the chars as part of a single token *)
- let translated =
- match tt.node with
- | Some tok -> Buffer.clear buff; tok
- | None -> translated in
- flush_buffer was_symbolchar tag translated;
- restart_buffering ()
+ (* A strong tag comes from Coq; if different Coq tags *)
+ (* hence, we don't try to see the chars as part of a single token *)
+ let translated =
+ match tt.node with
+ | Some tok -> Buffer.clear buff; tok
+ | None -> translated in
+ flush_buffer was_symbolchar tag translated;
+ restart_buffering ()
else
- begin
- (* If we change the category of characters (symbol vs ident) *)
- (* we accept this as a possible token cut point and remember the *)
- (* translated token up to that point *)
- let translated =
- if is_symbolchar <> was_symbolchar then
- match tt.node with
- | Some tok -> Buffer.clear buff; tok
- | None -> translated
- else translated in
- (* We try to make a significant token from the current *)
- (* buffer and the new character *)
- try
- let tt = ttree_descend tt c in
- Buffer.add_char buff c;
- Buffering (is_symbolchar,ctag,translated,tt)
- with Not_found ->
- (* No existing translation for the given set of chars *)
- if is_symbolchar <> was_symbolchar then
- (* If we changed the category of character read, we accept it *)
- (* as a possible cut point and restart looking for a translation *)
- (flush_buffer was_symbolchar tag translated;
- restart_buffering ())
- else
- (* If we did not change the category of character read, we do *)
- (* not want to cut arbitrarily in the middle of the sequence of *)
- (* symbol characters or identifier characters *)
- (Buffer.add_char buff c;
- Buffering (is_symbolchar,tag,translated,empty_ttree))
- end
+ begin
+ (* If we change the category of characters (symbol vs ident) *)
+ (* we accept this as a possible token cut point and remember the *)
+ (* translated token up to that point *)
+ let translated =
+ if is_symbolchar <> was_symbolchar then
+ match tt.node with
+ | Some tok -> Buffer.clear buff; tok
+ | None -> translated
+ else translated in
+ (* We try to make a significant token from the current *)
+ (* buffer and the new character *)
+ try
+ let tt = ttree_descend tt c in
+ Buffer.add_char buff c;
+ Buffering (is_symbolchar,ctag,translated,tt)
+ with Not_found ->
+ (* No existing translation for the given set of chars *)
+ if is_symbolchar <> was_symbolchar then
+ (* If we changed the category of character read, we accept it *)
+ (* as a possible cut point and restart looking for a translation *)
+ (flush_buffer was_symbolchar tag translated;
+ restart_buffering ())
+ else
+ (* If we did not change the category of character read, we do *)
+ (* not want to cut arbitrarily in the middle of the sequence of *)
+ (* symbol characters or identifier characters *)
+ (Buffer.add_char buff c;
+ Buffering (is_symbolchar,tag,translated,empty_ttree))
+ end
and restart_buffering () =
let tt = try ttree_descend !(!token_tree) c with Not_found -> empty_ttree in
@@ -163,9 +163,9 @@ let flush_sublexer () =
| Neutral -> ()
| Buffering (was_symbolchar,tag,translated,tt) ->
let translated =
- match tt.node with
- | Some tok -> Buffer.clear buff; tok
- | None -> translated in
+ match tt.node with
+ | Some tok -> Buffer.clear buff; tok
+ | None -> translated in
flush_buffer was_symbolchar tag translated;
translation_state := Neutral
diff --git a/tools/coqworkmgr.ml b/tools/coqworkmgr.ml
index 9f9c6dd5d0..343a61f44d 100644
--- a/tools/coqworkmgr.ml
+++ b/tools/coqworkmgr.ml
@@ -58,7 +58,7 @@ let read_fd fd s ~off ~len =
let rec loop () =
try Unix.read fd s off len
with Unix.Unix_error(Unix.EAGAIN,_,_) -> loop ()
- in
+ in
loop ()
let really_read_fd fd s off len =
@@ -129,10 +129,10 @@ let chat s =
try
match parse_request (raw_input_line party.sock) with
| Get n ->
- if !cur_tokens < !max_tokens then allocate n party
+ if !cur_tokens < !max_tokens then allocate n party
else Queue.push (n,party) queue
| TryGet n ->
- if !cur_tokens < !max_tokens then allocate n party
+ if !cur_tokens < !max_tokens then allocate n party
else answer party Noluck
| GiveBack n -> de_allocate n party
| Ping ->
@@ -192,7 +192,7 @@ let main () =
let pid = Unix.fork () in
if pid <> 0 then begin
Printf.printf "COQWORKMGR_SOCK=%s\n%!" str;
- exit 0
+ exit 0
end else begin
ignore(Unix.setsid ());
Unix.close Unix.stdin;
--
cgit v1.2.3