From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:01 +0200 Subject: Imported Upstream version 8.4dfsg --- tools/compat5.ml | 2 +- tools/compat5.mlp | 2 +- tools/compat5b.ml | 2 +- tools/compat5b.mlp | 2 +- tools/coq_makefile.ml | 6 +- tools/coq_tex.ml4 | 2 +- tools/coqdep.ml | 2 +- tools/coqdep_boot.ml | 2 +- tools/coqdep_common.ml | 2 +- tools/coqdep_common.mli | 2 +- tools/coqdep_lexer.mli | 2 +- tools/coqdep_lexer.mll | 2 +- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 2 +- tools/coqdoc/cpretty.mli | 2 +- tools/coqdoc/cpretty.mll | 71 +++++++++++++++++----- tools/coqdoc/index.ml | 13 +++- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 2 +- tools/coqdoc/output.ml | 151 ++++++++++++++++++++++++++++++++++++---------- tools/coqdoc/output.mli | 13 ++-- tools/coqdoc/tokens.ml | 2 +- tools/coqdoc/tokens.mli | 2 +- tools/coqwc.mll | 2 +- tools/escape_string.ml | 1 + tools/fake_ide.ml | 2 +- tools/gallina.ml | 2 +- tools/gallina_lexer.mll | 2 +- tools/mingwpath.ml | 15 +++++ 30 files changed, 238 insertions(+), 78 deletions(-) create mode 100644 tools/escape_string.ml create mode 100644 tools/mingwpath.ml (limited to 'tools') diff --git a/tools/compat5.ml b/tools/compat5.ml index 641d80d8..663f8d44 100644 --- a/tools/compat5.ml +++ b/tools/compat5.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* !r), start_env, stop_env + + let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph + let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote + + let url_buffer = Buffer.create 40 + let url_name_buffer = Buffer.create 40 let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos; lexbuf.lex_curr_p <- lexbuf.lex_start_p @@ -254,7 +263,7 @@ let nbsp,isp = count_spaces s in Output.indentation nbsp; let s = String.sub s isp (String.length s - isp) in - Output.ident s (lexeme_start lexbuf + isp) + Output.keyword s (lexeme_start lexbuf + isp) } @@ -369,13 +378,17 @@ let commands = | "Drop" | "ProtectedLoop" | "Quit" + | "Restart" | "Load" | "Add" | "Remove" space+ "Loadpath" | "Print" | "Inspect" | "About" + | "SearchAbout" + | "SearchRewrite" | "Search" + | "Locate" | "Eval" | "Reset" | "Check" @@ -403,6 +416,14 @@ let prog_kw = | "Obligations" | "Solve" +let hint_kw = + "Extern" | "Rewrite" | "Resolve" | "Immediate" | "Transparent" | "Opaque" | "Unfold" | "Constructors" + +let set_kw = + "Printing" space+ ("Coercions" | "Universes" | "All") + | "Implicit" space+ "Arguments" + + let gallina_kw_to_hide = "Implicit" space+ "Arguments" | "Ltac" @@ -410,15 +431,16 @@ let gallina_kw_to_hide = | "Import" | "Export" | "Load" - | "Hint" + | "Hint" space+ hint_kw | "Open" | "Close" | "Delimit" | "Transparent" | "Opaque" | ("Declare" space+ ("Morphism" | "Step") ) - | ("Set" | "Unset") space+ "Printing" space+ "Coercions" + | ("Set" | "Unset") space+ set_kw | "Declare" space+ ("Left" | "Right") space+ "Step" + | "Debug" space+ ("On" | "Off") let section = "*" | "**" | "***" | "****" @@ -689,7 +711,7 @@ and doc_bol = parse | space* nl+ { Output.paragraph (); doc_bol lexbuf } | "<<" space* - { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf } + { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf } | eof { true } | '_' @@ -713,8 +735,8 @@ and doc_list_bol indents = parse backtrack lexbuf; doc_bol lexbuf } | "<<" space* - { Output.start_verbatim (); - verbatim lexbuf; + { Output.start_verbatim false; + verbatim false lexbuf; doc_list_bol indents lexbuf } | "[[" nl { formatted := true; @@ -813,6 +835,7 @@ and doc indents = parse { inf_rules indents lexbuf } | "[]" { Output.proofbox (); doc indents lexbuf } + | "{{" { url lexbuf; doc indents lexbuf } | "[" { if !Cdglobals.plain_comments then Output.char '[' else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf; @@ -872,6 +895,15 @@ and doc indents = parse { if !Cdglobals.plain_comments then Output.char '_' else stop_emph () ; Output.char (lexeme_char lexbuf 1); doc indents lexbuf } + | "<<" space* + { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf } + | '"' + { if !Cdglobals.plain_comments + then Output.char '"' + else if in_quote () + then stop_quote () + else start_quote (); + doc indents lexbuf } | eof { false } | _ @@ -898,11 +930,22 @@ and escaped_html = parse | eof { () } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim = parse - | nl ">>" space* nl { Output.verbatim_char '\n'; Output.stop_verbatim () } - | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () } - | eof { Output.stop_verbatim () } - | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf } +and verbatim inline = parse + | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } + | ">>" { Output.stop_verbatim inline } + | eof { Output.stop_verbatim inline } + | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf } + +and url = parse + | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } + | "}" { url_name lexbuf } + | _ { Buffer.add_char url_buffer (lexeme_char lexbuf 0); url lexbuf } + +and url_name = parse + | "}" { Output.url (Buffer.contents url_buffer) (Some (Buffer.contents url_name_buffer)); + Buffer.clear url_buffer; Buffer.clear url_name_buffer } + | _ { Buffer.add_char url_name_buffer (lexeme_char lexbuf 0); url_name lexbuf } (*s Coq, inside quotations *) diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index f19433e9..d319ce72 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* for loc=loc1 to loc2 do - add_ref !cur_mod loc lib_dp sp id (type_of_string ty) + add_ref !cur_mod loc lib_dp sp id (type_of_string ty); + + (* Also add an entry for each module mentioned in [lib_dp], + * to use in interpolation. *) + ignore (List.fold_right (fun thisPiece priorPieces -> + let newPieces = match priorPieces with + | "" -> thisPiece + | _ -> thisPiece ^ "." ^ priorPieces in + add_ref !cur_mod loc "" "" newPieces Library; + newPieces) (Str.split (Str.regexp_string ".") lib_dp) "") done) with _ -> ()) | _ -> diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index bb775d26..8c658a90 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Buffer.add_char buff '\\'; Buffer.add_char buff c; Buffer.add_string buff "{}" + | '\'' -> + if i < String.length s - 1 && s.[i+1] = '\'' then begin + Buffer.add_char buff '\''; Buffer.add_char buff '{'; + Buffer.add_char buff '}' + end else + Buffer.add_char buff '\'' | c -> Buffer.add_char buff c done; @@ -282,9 +300,23 @@ module Latex = struct let stop_latex_math () = output_char '$' - let start_verbatim () = printf "\\begin{verbatim}" + let start_quote () = output_char '`'; output_char '`' + let stop_quote () = output_char '\''; output_char '\'' + + let start_verbatim inline = + if inline then printf "\\texttt{" + else printf "\\begin{verbatim}" - let stop_verbatim () = printf "\\end{verbatim}\n" + let stop_verbatim inline = + if inline then printf "}" + else printf "\\end{verbatim}\n" + + let url addr name = + printf "%s\\footnote{\\url{%s}}" + (match name with + | None -> "" + | Some n -> n) + addr let indentation n = if n == 0 then @@ -342,11 +374,19 @@ module Latex = struct | Some ref -> reference s ref | None -> if issymbchar then output_string s else printf "\\coqdocvar{%s}" s + let last_was_in = ref false + let sublexer c loc = - let tag = - try Some (Index.find (get_module false) loc) with Not_found -> None - in - Tokens.output_tagged_symbol_char tag c + if c = '*' && !last_was_in then begin + Tokens.flush_sublexer (); + output_char '*' + end else begin + let tag = + try Some (Index.find (get_module false) loc) with Not_found -> None + in + Tokens.output_tagged_symbol_char tag c + end; + last_was_in := false let initialize () = Tokens.token_tree := token_tree_latex; @@ -357,7 +397,11 @@ module Latex = struct let translate s = match Tokens.translate s with Some s -> s | None -> escaped s + let keyword s loc = + printf "\\coqdockw{%s}" (translate s) + let ident s loc = + last_was_in := s = "in"; try let tag = Index.find (get_module false) loc in reference (translate s) tag @@ -559,8 +603,22 @@ module Html = struct let start_latex_math () = () let stop_latex_math () = () - let start_verbatim () = printf "
"
-  let stop_verbatim () = printf "
\n" + let start_quote () = char '"' + let stop_quote () = start_quote () + + let start_verbatim inline = + if inline then printf "" + else printf "
"
+
+  let stop_verbatim inline = 
+    if inline then printf "" 
+    else printf "
\n" + + let url addr name = + printf "%s" addr + (match name with + | Some n -> n + | None -> addr) let module_ref m s = match find_module m with @@ -615,6 +673,9 @@ module Html = struct let translate s = match Tokens.translate s with Some s -> s | None -> escaped s + let keyword s loc = + printf "%s" (translate s) + let ident s loc = if is_keyword s then begin printf "%s" (translate s) @@ -915,19 +976,28 @@ module TeXmacs = struct let stop_latex_math () = output_char '>' - let start_verbatim () = in_doc := true; printf "<\\verbatim>" + let start_verbatim inline = in_doc := true; printf "<\\verbatim>" + let stop_verbatim inline = in_doc := false; printf "" - let stop_verbatim () = in_doc := false; printf "" + let url addr name = + printf "%s<\\footnote><\\url>%s" addr + (match name with + | None -> "" + | Some n -> n) + + let start_quote () = output_char '`'; output_char '`' + let stop_quote () = output_char '\''; output_char '\'' let indentation n = () + let keyword s = + printf "" + let ident_true s = - if is_keyword s then begin - printf "" - end else begin - raw_ident s - end + if is_keyword s then keyword s + else raw_ident s + let keyword s loc = keyword s let ident s _ = if !in_doc then ident_true s else raw_ident s let output_sublexer_string doescape issymbchar tag s = @@ -1042,13 +1112,21 @@ module Raw = struct let start_latex_math () = () let stop_latex_math () = () - let start_verbatim () = () + let start_verbatim inline = () + let stop_verbatim inline = () + + let url addr name = + match name with + | Some n -> printf "%s (%s)" n addr + | None -> printf "%s" addr - let stop_verbatim () = () + let start_quote () = printf "\"" + let stop_quote () = printf "\"" let indentation n = for i = 1 to n do printf " " done + let keyword s loc = raw_ident s let ident s loc = raw_ident s let sublexer c l = char c @@ -1162,6 +1240,7 @@ let rule = select Latex.rule Html.rule TeXmacs.rule Raw.rule let nbsp = select Latex.nbsp Html.nbsp TeXmacs.nbsp Raw.nbsp let char = select Latex.char Html.char TeXmacs.char Raw.char +let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize @@ -1189,12 +1268,20 @@ let start_verbatim = select Latex.start_verbatim Html.start_verbatim TeXmacs.start_verbatim Raw.start_verbatim let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim Raw.stop_verbatim -let verbatim_char = - select output_char Html.char TeXmacs.char Raw.char +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 = + select Latex.url Html.url TeXmacs.url Raw.url + +let start_quote = + select Latex.start_quote Html.start_quote TeXmacs.start_quote Raw.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 = - start_verbatim (); + start_verbatim false; let dumb_line = function (sp,ln) -> (String.iter char ((String.make sp ' ') ^ ln); char '\n') @@ -1204,7 +1291,7 @@ let inf_rule_dumb assumptions (midsp,midln,midnm) conclusions = | Some s -> " " ^ s | None -> "")); List.iter dumb_line conclusions); - stop_verbatim () + stop_verbatim false let inf_rule = select inf_rule_dumb Html.inf_rule inf_rule_dumb inf_rule_dumb diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 53d88666..80f39011 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit val nbsp : unit -> unit val char : char -> unit +val keyword : string -> loc -> unit val ident : string -> loc -> unit val sublexer : char -> loc -> unit val initialize : unit -> unit @@ -70,13 +71,17 @@ val latex_char : char -> unit val latex_string : string -> unit val html_char : char -> unit val html_string : string -> unit -val verbatim_char : char -> unit +val verbatim_char : bool -> char -> unit val hard_verbatim_char : char -> unit val start_latex_math : unit -> unit val stop_latex_math : unit -> unit -val start_verbatim : unit -> unit -val stop_verbatim : unit -> unit +val start_verbatim : bool -> unit +val stop_verbatim : bool -> unit +val start_quote : unit -> unit +val stop_quote : unit -> unit + +val url : string -> string option -> unit (* this outputs an inference rule in one go. You pass it the list of assumptions, then the middle line info, then the conclusion (which diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml index a228797e..10a105f9 100644 --- a/tools/coqdoc/tokens.ml +++ b/tools/coqdoc/tokens.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*