From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coqdoc/output.ml | 234 ++++++++++++++++++++++++------------------------- 1 file changed, 117 insertions(+), 117 deletions(-) (limited to 'tools/coqdoc/output.ml') diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 302cbffce..0c5e9ff29 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -25,26 +25,26 @@ let sprintf = Printf.sprintf (*s Coq keywords *) -let build_table l = +let build_table l = let h = Hashtbl.create 101 in List.iter (fun key ->Hashtbl.add h key ()) l; function s -> try Hashtbl.find h s; true with Not_found -> false -let is_keyword = +let is_keyword = build_table [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; - "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; + "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; - "Hypothesis"; "Hypotheses"; - "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; + "Hypothesis"; "Hypotheses"; + "Resolve"; "Unfold"; "Immediate"; "Extern"; "Implicit"; "Import"; "Inductive"; + "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; + "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; - "Delimit"; "Bind"; "Open"; "Scope"; + "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; "Implicit Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation"; @@ -54,13 +54,13 @@ let is_keyword = "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; "Program Instance"; "Equations"; "Equations_nocomp"; (*i (* coq terms *) *) - "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; + "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; (* Ltac *) "before"; "after" ] -let is_tactic = +let is_tactic = build_table [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; @@ -81,14 +81,14 @@ let current_module : (string * string option) ref = ref ("",None) let get_module withsub = let (m,sub) = !current_module in - if withsub then - match sub with + if withsub then + match sub with | None -> m | Some sub -> m ^ ": " ^ sub else m -let set_module m sub = current_module := (m,sub); +let set_module m sub = current_module := (m,sub); page_title := get_module true (*s Common to both LaTeX and HTML *) @@ -102,15 +102,15 @@ let token_pp = Hashtbl.create 97 let add_printing_token = Hashtbl.replace token_pp -let find_printing_token tok = +let find_printing_token tok = try Hashtbl.find token_pp tok with Not_found -> None, None let remove_printing_token = Hashtbl.remove token_pp (* predefined pretty-prints *) -let initialize () = +let initialize () = let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in - List.iter + List.iter (fun (s,l,l') -> Hashtbl.add token_pp s (Some l, l')) [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; "|", "\\ensuremath{|}", None; @@ -136,7 +136,7 @@ let initialize () = (*s Table of contents *) -type toc_entry = +type toc_entry = | Toc_library of string * string option | Toc_section of int * (unit -> unit) * string @@ -172,7 +172,7 @@ module Latex = struct Queue.iter (fun s -> printf "%s\n" s) preamble; printf "\\begin{document}\n" end; - output_string + output_string "%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\n"; output_string "%% This file has been automatically generated with the command\n"; @@ -188,19 +188,19 @@ module Latex = struct end let char c = match c with - | '\\' -> + | '\\' -> printf "\\symbol{92}" - | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> + | '$' | '#' | '%' | '&' | '{' | '}' | '_' -> output_char '\\'; output_char c - | '^' | '~' -> + | '^' | '~' -> output_char '\\'; output_char c; printf "{}" - | _ -> + | _ -> output_char c let label_char c = match c with | '\\' | '$' | '#' | '%' | '&' | '{' | '}' | '_' | '^' | '~' -> () - | _ -> + | _ -> output_char c let latex_char = output_char @@ -215,10 +215,10 @@ module Latex = struct let label_ident s = for i = 0 to String.length s - 1 do label_char s.[i] done - let start_module () = + let start_module () = let ln = !lib_name in if not !short then begin - printf "\\coqlibrary{"; + printf "\\coqlibrary{"; label_ident (get_module false); printf "}{"; if ln <> "" then printf "%s " ln; @@ -235,22 +235,22 @@ module Latex = struct let stop_verbatim () = printf "\\end{verbatim}\n" - let indentation n = - if n == 0 then + let indentation n = + if n == 0 then printf "\\coqdocnoindent\n" else let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space let with_latex_printing f tok = - try + try (match Hashtbl.find token_pp tok with | Some s, _ -> output_string s | _ -> f tok) - with Not_found -> + with Not_found -> f tok - let module_ref m s = + let module_ref m s = printf "\\moduleid{%s}{" m; raw_ident s; printf "}" (*i match find_module m with @@ -278,16 +278,16 @@ module Latex = struct printf "\\coq%s{" (type_name ty); label_ident (m ^ "." ^ id); printf "}{"; raw_ident s; printf "}" let reference s = function - | Def (fullid,typ) -> + | Def (fullid,typ) -> defref (get_module false) fullid typ s | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid,typ) -> + | Ref (m,fullid,typ) -> ident_ref m fullid typ s | Mod _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" - - let ident s loc = + + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" end else begin @@ -298,7 +298,7 @@ module Latex = struct if is_tactic s then begin printf "\\coqdoctac{"; raw_ident s; printf "}" end else begin - if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try reference s (Index.find_string (get_module false) s) with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}") @@ -307,19 +307,19 @@ module Latex = struct end end - let ident s l = + let ident s l = if !in_title then ( printf "\\texorpdfstring{\\protect"; with_latex_printing (fun s -> ident s l) s; printf "}{"; raw_ident s; printf "}") else with_latex_printing (fun s -> ident s l) s - + let symbol s = with_latex_printing raw_ident s let proofbox () = printf "\\ensuremath{\\Box}" - let rec reach_item_level n = + let rec reach_item_level n = if !item_level < n then begin printf "\n\\begin{itemize}\n\\item "; incr item_level; reach_item_level n @@ -397,14 +397,14 @@ end (*s HTML output *) module Html = struct - + let header () = if !header_trailer then if !header_file_spec then let cin = Pervasives.open_in !header_file in - try - while true do - let s = Pervasives.input_line cin in + try + while true do + let s = Pervasives.input_line cin in printf "%s\n" s done with End_of_file -> Pervasives.close_in cin @@ -421,14 +421,14 @@ module Html = struct end let trailer () = - if !index && (get_module false) <> "Index" then + if !index && (get_module false) <> "Index" then printf "\n\n
\n
Index" !index_name; - if !header_trailer then + if !header_trailer then if !footer_file_spec then let cin = Pervasives.open_in !footer_file in - try - while true do - let s = Pervasives.input_line cin in + try + while true do + let s = Pervasives.input_line cin in printf "%s\n" s done with End_of_file -> Pervasives.close_in cin @@ -439,7 +439,7 @@ module Html = struct printf "
\n\n\n\n\n" end - let start_module () = + let start_module () = let ln = !lib_name in if not !short then begin let (m,sub) = !current_module in @@ -454,7 +454,7 @@ module Html = struct let line_break () = printf "
\n" - let empty_line_of_code () = + let empty_line_of_code () = printf "\n
\n" let char = function @@ -477,7 +477,7 @@ module Html = struct let start_verbatim () = printf "
"
   let stop_verbatim () = printf "
\n" - let module_ref m s = + let module_ref m s = match find_module m with | Local -> printf "" m; raw_ident s; printf "" @@ -491,56 +491,56 @@ module Html = struct match find_module m with | Local -> printf "" m fid; - printf "" typ; + printf "" typ; raw_ident s; printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in printf "" m fid; - printf "" typ; + printf "" typ; raw_ident s; printf "" | Coqlib | Unknown -> printf "" typ; raw_ident s; printf "" - - let reference s r = + + let reference s r = match r with - | Def (fullid,ty) -> - printf "" fullid; - printf "" (type_name ty); + | Def (fullid,ty) -> + printf "" fullid; + printf "" (type_name ty); raw_ident s; printf "" | Mod (m,s') when s = s' -> module_ref m s - | Ref (m,fullid,ty) -> + | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s | Mod _ -> printf ""; raw_ident s ; printf "" - let ident s loc = + let ident s loc = if is_keyword s then begin - printf ""; - raw_ident s; + printf ""; + raw_ident s; printf "" - end else + end else begin try reference s (Index.find (get_module false) loc) with Not_found -> if is_tactic s then (printf ""; raw_ident s; printf "") else - if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try reference s (Index.find_string (get_module false) s) with _ -> (printf ""; raw_ident s ; printf "") else (printf ""; raw_ident s ; printf "") end - + let with_html_printing f tok = - try + try (match Hashtbl.find token_pp tok with | _, Some s -> output_string s | _ -> f tok) - with Not_found -> + with Not_found -> f tok let ident s l = @@ -551,7 +551,7 @@ module Html = struct let proofbox () = printf "☐" - let rec reach_item_level n = + let rec reach_item_level n = if !item_level < n then begin printf "