diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 3 | ||||
| -rw-r--r-- | tools/coq_dune.ml | 301 | ||||
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 239 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 24 | ||||
| -rw-r--r-- | tools/coqdoc/output.mli | 3 | ||||
| -rw-r--r-- | tools/dune | 6 |
6 files changed, 192 insertions, 384 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index b8e498898b..597351db9b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -54,7 +54,7 @@ OCAMLWARN := $(COQMF_WARN) # # Parameters are make variable assignments. # They can be passed to (each call to) make on the command line. -# They can also be put in @LOCAL_FILE@ once an for all. +# They can also be put in @LOCAL_FILE@ once and for all. # For retro-compatibility reasons they can be put in the _CoqProject, but this # practice is discouraged since _CoqProject better not contain make specific # code (be nice to user interfaces). @@ -616,6 +616,7 @@ cleanall:: clean $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache .PHONY: cleanall archclean:: diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml deleted file mode 100644 index 472e6b4948..0000000000 --- a/tools/coq_dune.ml +++ /dev/null @@ -1,301 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* <O___,, * (see version control and CREDITS file for authors & dates) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* LICENSE NOTE: This file is dually MIT/LGPL 2.1+ licensed. MIT license: - * - * Permission is hereby granted, free of charge, to any person obtaining a copy - * of this software and associated documentation files (the "Software"), to deal - * in the Software without restriction, including without limitation the rights - * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell - * copies of the Software, and to permit persons to whom the Software is - * furnished to do so, subject to the following conditions: - * - * The above copyright notice and this permission notice shall be included in all - * copies or substantial portions of the Software. - * - * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR - * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, - * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE - * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER - * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, - * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE - * SOFTWARE. - *) - -(* coq_dune: generate dune build rules for .vo files *) -(* *) -(* At some point this file will become a Dune plugin, so it is very *) -(* important that this file can be bootstrapped with: *) -(* *) -(* ocamlfind ocamlopt -linkpkg -package str coq_dune.ml -o coq_dune *) - -open Format - -(* Keeping this file self-contained as it is a "bootstrap" utility *) -(* Is OCaml missing these basic functions in the stdlib? *) -module Aux = struct - - let option_iter f o = match o with - | Some x -> f x - | None -> () - - let option_cata d f o = match o with - | Some x -> f x - | None -> d - - let list_compare f = let rec lc x y = match x, y with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x::xs, y::ys -> let r = f x y in if r = 0 then lc xs ys else r - in lc - - let rec pp_list pp sep fmt l = match l with - | [] -> () - | [l] -> fprintf fmt "%a" pp l - | x::xs -> fprintf fmt "%a%a%a" pp x sep () (pp_list pp sep) xs - - let rec pmap f l = match l with - | [] -> [] - | x :: xs -> - begin match f x with - | None -> pmap f xs - | Some r -> r :: pmap f xs - end - - let sep fmt () = fprintf fmt "@;" - - (* Creation of paths, aware of the platform separator. *) - let bpath l = String.concat Filename.dir_sep l - - module DirOrd = struct - type t = string list - let compare = list_compare String.compare - end - - module DirMap = Map.Make(DirOrd) - - (* Functions available in newer OCaml versions *) - (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) - module Legacy = struct - - - (* Fix once we move to OCaml >= 4.06.0 *) - let list_init len f = - let rec init_aux i n f = - if i >= n then [] - else let r = f i in r :: init_aux (i+1) n f - in init_aux 0 len f - - (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) - let dirmap_update key f map = - match begin - try f (Some (DirMap.find key map)) - with Not_found -> f None - end with - | None -> DirMap.remove key map - | Some x -> DirMap.add key x map - - end - - let add_map_list key elem map = - (* Move to Dirmap.update once we require OCaml >= 4.06.0 *) - Legacy.dirmap_update key (fun l -> Some (option_cata [elem] (fun ll -> elem :: ll) l)) map - - let replace_ext ~file ~newext = - Filename.(remove_extension file) ^ newext - -end - -open Aux - -(* Once this is a Dune plugin the flags will be taken from the env *) -module Options = struct - - type flag = { - enabled : bool; - cmd : string; - } - - let all_opts = - [ { enabled = false; cmd = "-debug"; } - ; { enabled = false; cmd = "-native_compiler"; } - ; { enabled = true; cmd = "-w +default"; } - ] - - let build_coq_flags () = - let popt o = if o.enabled then Some o.cmd else None in - String.concat " " @@ pmap popt all_opts -end - -type vodep = { - target: string; - deps : string list; -} - -type ldep = | VO of vodep | MLG of string -type ddir = ldep list DirMap.t - -(* Filter `.vio` etc... *) -let filter_no_vo = - List.filter (fun f -> Filename.check_suffix f ".vo") - -(* We could have coqdep to output dune files directly *) - -let gen_sub n = - (* Move to List.init once we can depend on OCaml >= 4.06.0 *) - bpath @@ Legacy.list_init n (fun _ -> "..") - -let pp_rule fmt targets deps action = - (* Special printing of the first rule *) - let ppl = pp_list pp_print_string sep in - let pp_deps fmt l = match l with - | [] -> - () - | x :: xs -> - fprintf fmt "(:pp-file %s)%a" x sep (); - pp_list pp_print_string sep fmt xs - in - fprintf fmt - "@[(rule@\n @[(targets @[%a@])@\n(deps @[%a@])@\n(action @[%a@])@])@]@\n" - ppl targets pp_deps deps pp_print_string action - -let gen_coqc_targets vo = - [ vo.target - ; replace_ext ~file:vo.target ~newext:".glob" - ; replace_ext ~file:vo.target ~newext:".vos" - ; "." ^ replace_ext ~file:vo.target ~newext:".aux"] - -(* Generate the dune rule: *) -let pp_vo_dep dir fmt vo = - let depth = List.length dir in - let sdir = gen_sub depth in - (* All files except those in Init implicitly depend on the Prelude, we account for it here. *) - let eflag, edep = if List.tl dir = ["Init"] then "-noinit -R theories Coq", [] else "", [bpath ["theories";"Init";"Prelude.vo"]] in - (* Coq flags *) - let cflag = Options.build_coq_flags () in - (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) - let deps = List.map (fun s -> bpath [sdir;s]) (edep @ vo.deps) in - (* The source file is also corrected as we will call coqtop from the top dir *) - let source = bpath (dir @ [replace_ext ~file:vo.target ~newext:".v"]) in - (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *) - let libflag = "-coqlib %{project_root}" in - (* The final build rule *) - let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in - let all_targets = gen_coqc_targets vo in - pp_rule fmt all_targets deps action - -let pp_mlg_dep _dir fmt ml = - fprintf fmt "@[(coq.pp (modules %s))@]@\n" (Filename.remove_extension ml) - -let pp_dep dir fmt oo = match oo with - | VO vo -> pp_vo_dep dir fmt vo - | MLG f -> pp_mlg_dep dir fmt f - -let out_install fmt dir ff = - let itarget = String.concat "/" dir in - let ff = List.concat @@ pmap (function | VO vo -> Some (gen_coqc_targets vo) | _ -> None) ff in - let pp_ispec fmt tg = fprintf fmt "(%s as coq/%s)" tg (bpath [itarget;tg]) in - fprintf fmt "(install@\n @[(section lib_root)@\n(package coq)@\n(files @[%a@])@])@\n" - (pp_list pp_ispec sep) ff - -(* For each directory, we must record two things, the build rules and - the install specification. *) -let record_dune d ff = - let sd = bpath d in - if Sys.file_exists sd && Sys.is_directory sd then - let out = open_out (bpath [sd;"dune"]) in - let fmt = formatter_of_out_channel out in - if Sys.file_exists (bpath [sd; "plugin_base.dune"]) then - fprintf fmt "(include plugin_base.dune)@\n"; - out_install fmt d ff; - List.iter (pp_dep d fmt) ff; - fprintf fmt "%!"; - close_out out - else - eprintf "error in coq_dune, a directory disappeared: %s@\n%!" sd - -(* File Scanning *) -let scan_mlg ~root m d = - let dir = [root; d] in - let m = DirMap.add dir [] m in - let mlg = Sys.(List.filter (fun f -> Filename.(check_suffix f ".mlg")) - Array.(to_list @@ readdir (bpath dir))) in - List.fold_left (fun m f -> add_map_list [root; d] (MLG f) m) m mlg - -let scan_dir ~root m = - let is_plugin_directory dir = Sys.(is_directory dir && file_exists (bpath [dir;"plugin_base.dune"])) in - let dirs = Sys.(List.filter (fun f -> is_plugin_directory @@ bpath [root;f]) Array.(to_list @@ readdir root)) in - List.fold_left (scan_mlg ~root) m dirs - -let scan_plugins m = scan_dir ~root:"plugins" m -let scan_usercontrib m = scan_dir ~root:"user-contrib" m - -(* This will be removed when we drop support for Make *) -let fix_cmo_cma file = - if String.equal Filename.(extension file) ".cmo" - then replace_ext ~file ~newext:".cma" - else file - -(* Process .vfiles.d and generate a skeleton for the dune file *) -let parse_coqdep_line l = - match Str.(split (regexp ":") l) with - | [targets;deps] -> - let targets = Str.(split (regexp "[ \t]+") targets) in - let deps = Str.(split (regexp "[ \t]+") deps) in - let targets = filter_no_vo targets in - begin match targets with - | [target] -> - let dir, target = Filename.(dirname target, basename target) in - (* coqdep outputs with the '/' directory separator regardless of - the platform. Anyways, I hope we can link to coqdep instead - of having to parse its output soon, that should solve this - kind of issues *) - let deps = List.map fix_cmo_cma deps in - Some (String.split_on_char '/' dir, VO { target; deps; }) - (* Otherwise a vio file, we ignore *) - | _ -> None - end - (* Strange rule, we ignore *) - | _ -> None - -let rec read_vfiles ic map = - try - let rule = parse_coqdep_line (input_line ic) in - (* Add vo_entry to its corresponding map entry *) - let map = option_cata map (fun (dir, vo) -> add_map_list dir vo map) rule in - read_vfiles ic map - with End_of_file -> map - -let out_map map = - DirMap.iter record_dune map - -let exec_ifile f = - match Array.length Sys.argv with - | 1 -> f stdin - | 2 -> - let in_file = Sys.argv.(1) in - begin try - let ic = open_in in_file in - (try f ic - with exn -> - eprintf "Error: exec_ifile @[%s@]@\n%!" (Printexc.to_string exn); - close_in ic) - with _ -> - eprintf "Error: cannot open input file %s@\n%!" in_file - end - | _ -> eprintf "Error: wrong number of arguments@\n%!"; exit 1 - -let _ = - exec_ifile (fun ic -> - let map = scan_plugins DirMap.empty in - let map = scan_usercontrib map in - let map = read_vfiles ic map in - out_map map) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 210ac754a1..86d213453b 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -32,6 +32,19 @@ in count 0 0 + let count_newlines s = + let len = String.length s in + let n = ref 0 in + String.iteri (fun i c -> + match c with (* skip "\r\n" *) + | '\r' when i + 1 = len || s.[i+1] = '\n' -> incr n + | '\n' -> incr n + | _ -> ()) s; + !n + + (* Whether a string starts with a newline (used on strings that might match the [nl] regexp) *) + let is_nl s = String.length s = 0 || let c = s.[0] in c = '\n' || c = '\r' + let remove_newline s = let n = String.length s in let rec count i = if i == n || s.[i] <> '\n' then i else count (i + 1) in @@ -65,8 +78,12 @@ let eol = s.[String.length s - 1] = '\n' in (eol, if eol then String.sub s 1 (String.length s - 1) else s) + let is_none x = + match x with + | None -> true + | Some _ -> false - let formatted = ref false + let formatted : position option ref = ref None let brackets = ref 0 let comment_level = ref 0 let in_proof = ref None @@ -116,10 +133,15 @@ let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () + let begin_details s = + save_state (); Cdglobals.gallina := false; Cdglobals.light := false; + Output.start_details s + let end_details () = Output.stop_details (); restore_state () + (* Reset the globals *) let reset () = - formatted := false; + formatted := None; brackets := 0; comment_level := 0 @@ -247,13 +269,28 @@ let parse_comments () = !Cdglobals.parse_comments && not (only_gallina ()) + (* Advance lexbuf by n lines. Equivalent to calling [Lexing.new_line lexbuf] n times *) + let new_lines n lexbuf = + let lcp = lexbuf.lex_curr_p in + if lcp != dummy_pos then + lexbuf.lex_curr_p <- + { lcp with + pos_lnum = lcp.pos_lnum + n; + pos_bol = lcp.pos_cnum } + + let print_position chan p = + Printf.fprintf chan "%s:%d:%d" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol) + + exception MismatchPreformatted of position + + (* let debug lexbuf msg = Printf.printf "%a %s\n" print_position lexbuf.lex_start_p msg *) } (*s Regular expressions *) let space = [' ' '\t'] -let space_nl = [' ' '\t' '\n' '\r'] -let nl = "\r\n" | '\n' +let nl = "\r\n" | '\n' | '\r' +let space_nl = space | nl let firstchar = ['A'-'Z' 'a'-'z' '_'] | @@ -430,10 +467,12 @@ let section = "*" | "**" | "***" | "****" let item_space = " " -let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl -let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl -let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl -let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl +let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* +let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* +let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* +let end_show = "(*" space* "end" space+ "show" space* "*)" space* +let begin_details = "(*" space* "begin" space+ "details" space* +let end_details = "(*" space* "end" space+ "details" space* "*)" space* (* let begin_verb = "(*" space* "begin" space+ "verb" space* "*)" let end_verb = "(*" space* "end" space+ "verb" space* "*)" @@ -442,24 +481,36 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" (*s Scanning Coq, at beginning of line *) rule coq_bol = parse - | space* nl+ - { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) + | space* (nl+ as s) + { new_lines (String.length s) lexbuf; + if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf } - | space* "(**" space_nl - { Output.end_coq (); Output.start_doc (); + | space* "(**" (space_nl as s) + { if is_nl s then Lexing.new_line lexbuf; + Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } - | space* "Comments" space_nl - { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); - Output.start_coq (); coq lexbuf } - | space* begin_hide - { skip_hide lexbuf; coq_bol lexbuf } - | space* begin_show - { begin_show (); coq_bol lexbuf } - | space* end_show - { end_show (); coq_bol lexbuf } + | space* "Comments" (space_nl as s) + { if is_nl s then Lexing.new_line lexbuf; + Output.end_coq (); Output.start_doc (); + comments lexbuf; + Output.end_doc (); Output.start_coq (); + coq lexbuf } + | space* begin_hide nl + { Lexing.new_line lexbuf; skip_hide lexbuf; coq_bol lexbuf } + | space* begin_show nl + { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf } + | space* end_show nl + { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf } + | space* begin_details nl + { Lexing.new_line lexbuf; + let s = details_body lexbuf in + Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf } + | space* end_details nl + { Lexing.new_line lexbuf; + Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf } | space* (("Local"|"Global") space+)? gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then @@ -565,9 +616,10 @@ rule coq_bol = parse and coq = parse | nl - { if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } - | "(**" space_nl - { Output.end_coq (); Output.start_doc (); + { Lexing.new_line lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } + | "(**" (space_nl as s) + { if is_nl s then Lexing.new_line lexbuf; + Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then coq_bol lexbuf else coq lexbuf } @@ -579,8 +631,9 @@ and coq = parse comment lexbuf end else skipped_comment lexbuf in if eol then coq_bol lexbuf else coq lexbuf } - | nl+ space* "]]" - { if not !formatted then + | (nl+ as s) space* "]]" + { new_lines (count_newlines s) lexbuf; + if is_none !formatted then begin (* Isn't this an anomaly *) let s = lexeme lexbuf in @@ -665,8 +718,9 @@ and coq = parse (*s Scanning documentation, at beginning of line *) and doc_bol = parse - | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')? - { let eol, lex = strip_eol (lexeme lexbuf) in + | space* section space+ ([^'\n' '\r' '*'] | '*'+ [^'\n' '\r' ')' '*'])* ('*'+ (nl as s))? + { if not (is_none s) then Lexing.new_line lexbuf; + let eol, lex = strip_eol (lexeme lexbuf) in let lev, s = sec_title lex in if (!Cdglobals.lib_subtitles) && (subtitle (Output.get_module false) s) then @@ -674,24 +728,20 @@ and doc_bol = parse else Output.section lev (fun () -> ignore (doc None (from_string s))); if eol then doc_bol lexbuf else doc None lexbuf } - | space_nl* '-'+ - { let buf' = lexeme lexbuf in - let bufs = Str.split_delim (Str.regexp "['\n']") buf' in - let lines = (List.length bufs) - 1 in - let line = - match bufs with - | [] -> eprintf "Internal error bad_split1 - please report\n"; - exit 1 - | _ -> List.nth bufs lines - in - match check_start_list line with - | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> if lines > 0 then Output.paragraph (); - Output.item 1; doc (Some [n]) lexbuf - | Rule -> Output.rule (); doc None lexbuf + | (space_nl* as s) ('-'+ as line) + { let nl_count = count_newlines s in + match check_start_list line with + | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf + | List n -> + new_lines nl_count lexbuf; + if nl_count > 0 then Output.paragraph (); + Output.item 1; doc (Some [n]) lexbuf + | Rule -> + new_lines nl_count lexbuf; + Output.rule (); doc None lexbuf } - | space* nl+ - { Output.paragraph (); doc_bol lexbuf } + | (space_nl* nl) as s + { new_lines (count_newlines s) lexbuf; Output.paragraph (); doc_bol lexbuf } | "<<" space* { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf } | eof @@ -699,8 +749,7 @@ and doc_bol = parse | '_' { if !Cdglobals.plain_comments then Output.char '_' else start_emph (); doc None lexbuf } - | _ - { backtrack lexbuf; doc None lexbuf } + | "" { doc None lexbuf } (*s Scanning lists - using whitespace *) and doc_list_bol indents = parse @@ -721,11 +770,11 @@ and doc_list_bol indents = parse verbatim 0 false lexbuf; doc_list_bol indents lexbuf } | "[[" nl - { formatted := true; + { formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); ignore(body_bol lexbuf); Output.end_inline_coq_block (); - formatted := false; + formatted := None; doc_list_bol indents lexbuf } | "[[[" nl { inf_rules (Some indents) lexbuf } @@ -788,10 +837,10 @@ and doc indents = parse | "[[" nl { if !Cdglobals.plain_comments then (Output.char '['; Output.char '['; doc indents lexbuf) - else (formatted := true; + else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); let eol = body_bol lexbuf in - Output.end_inline_coq_block (); formatted := false; + Output.end_inline_coq_block (); formatted := None; if eol then match indents with | Some ls -> doc_list_bol ls lexbuf @@ -816,16 +865,15 @@ and doc indents = parse if !Cdglobals.parse_comments then comment lexbuf else skipped_comment lexbuf in if eol then bol_parse lexbuf else doc indents lexbuf } - | '*'* "*)" space_nl* "(**" - {(match indents with + | '*'* "*)" (space_nl* as s) "(**" + { let nl_count = count_newlines s in + new_lines nl_count lexbuf; + (match indents with | Some _ -> Output.stop_item () | None -> ()); (* this says - if there is a blank line between the two comments, insert one in the output too *) - let lines = List.length (Str.split_delim (Str.regexp "['\n']") - (lexeme lexbuf)) - in - if lines > 2 then Output.paragraph (); + if nl_count > 1 then Output.paragraph (); doc_bol lexbuf } | '*'* "*)" space* nl @@ -1017,10 +1065,10 @@ and comment = parse comment lexbuf } | "[[" nl { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') - else (formatted := true; + else (formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); let _ = body_bol lexbuf in - Output.end_inline_coq_block (); formatted := false); + Output.end_inline_coq_block (); formatted := None); comment lexbuf } | "$" { if !Cdglobals.plain_comments then Output.char '$' @@ -1083,13 +1131,14 @@ and skip_to_dot_or_brace = parse and body_bol = parse | space+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } - | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } + | "" { Output.indentation 0; body lexbuf } and body = parse | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf} - | nl+ space* "]]" space* nl - { Tokens.flush_sublexer(); - if not !formatted then + | (nl+ as s) space* "]]" space* nl + { new_lines (count_newlines s + 1) lexbuf; + Tokens.flush_sublexer(); + if is_none !formatted then begin let s = lexeme lexbuf in let nlsp,s = remove_newline s in @@ -1107,7 +1156,8 @@ and body = parse end } | "]]" space* nl { Tokens.flush_sublexer(); - if not !formatted then + Lexing.new_line lexbuf; + if is_none !formatted then begin let loc = lexeme_start lexbuf in Output.sublexer ']' loc; @@ -1121,13 +1171,19 @@ and body = parse Output.paragraph (); true end } - | eof { Tokens.flush_sublexer(); false } - | '.' space* nl | '.' space* eof - { Tokens.flush_sublexer(); Output.char '.'; Output.line_break(); - if not !formatted then true else body_bol lexbuf } + | eof + { Tokens.flush_sublexer(); + match !formatted with + | None -> false + | Some p -> raise (MismatchPreformatted p) } + | '.' space* (nl as s | eof) + { if not (is_none s) then new_line lexbuf; + Tokens.flush_sublexer(); Output.char '.'; Output.line_break(); + if is_none !formatted then true else body_bol lexbuf } | '.' space* nl "]]" space* nl - { Tokens.flush_sublexer(); Output.char '.'; - if not !formatted then + { new_lines 2 lexbuf; + Tokens.flush_sublexer(); Output.char '.'; + if is_none !formatted then begin eprintf "Error: stray ]] at %d\n" (lexeme_start lexbuf); flush stderr; @@ -1141,9 +1197,10 @@ and body = parse } | '.' space+ { Tokens.flush_sublexer(); Output.char '.'; Output.char ' '; - if not !formatted then false else body lexbuf } - | "(**" space_nl - { Tokens.flush_sublexer(); Output.end_coq (); Output.start_doc (); + if is_none !formatted then false else body lexbuf } + | "(**" (space_nl as s) + { if is_nl s then new_line lexbuf; + Tokens.flush_sublexer(); Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then body_bol lexbuf else body lexbuf } @@ -1208,19 +1265,37 @@ and string = parse | _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf } and skip_hide = parse - | eof | end_hide { () } + | eof | end_hide nl { Lexing.new_line lexbuf; () } | _ { skip_hide lexbuf } (*s Reading token pretty-print *) and printing_token_body = parse - | "*)" nl? | eof - { let s = Buffer.contents token_buffer in + | "*)" (nl as s)? | eof + { if not (is_none s) then Lexing.new_line lexbuf; + let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } - | _ { Buffer.add_string token_buffer (lexeme lexbuf); + | (nl | _) as s + { if is_nl s then Lexing.new_line lexbuf; + Buffer.add_string token_buffer (lexeme lexbuf); printing_token_body lexbuf } +and details_body = parse + | "*)" space* (nl as s)? | eof + { if not (is_none s) then Lexing.new_line lexbuf; + None } + | ":" space* { details_body_rec lexbuf } + +and details_body_rec = parse + | "*)" space* (nl as s)? | eof + { if not (is_none s) then Lexing.new_line lexbuf; + let s = Buffer.contents token_buffer in + Buffer.clear token_buffer; + Some s } + | _ { Buffer.add_string token_buffer (lexeme lexbuf); + details_body_rec lexbuf } + (*s These handle inference rules, parsing the body segments of things enclosed in [[[ ]]] brackets *) and inf_rules indents = parse @@ -1318,6 +1393,14 @@ and st_subtitle = parse (*s Applying the scanners to files *) { + (* coq_bol with error handling *) + let coq_bol' f lb = + Lexing.new_line lb; (* Start numbering lines from 1 *) + try coq_bol lb with + | MismatchPreformatted p -> + Printf.eprintf "%a: mismatched \"[[\"\n" print_position { p with pos_fname = f }; + exit 1 + let coq_file f m = reset (); let c = open_in f in @@ -1325,7 +1408,7 @@ and st_subtitle = parse (Index.current_library := m; Output.initialize (); Output.start_module (); - Output.start_coq (); coq_bol lb; Output.end_coq (); + Output.start_coq (); coq_bol' f lb; Output.end_coq (); close_in c) let detect_subtitle f m = diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d2b0078a7c..dd1b65d294 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -42,7 +42,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite"; + "Search"; "SearchHead"; "SearchPattern"; "SearchRewrite"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; @@ -469,6 +469,11 @@ module Latex = struct let stop_emph () = printf "}" + let start_details _ = () + + let stop_details () = () + + let start_comment () = printf "\\begin{coqdoccomment}\n" let end_comment () = printf "\\end{coqdoccomment}\n" @@ -740,6 +745,12 @@ module Html = struct let stop_emph () = printf "</i>" + let start_details = function + | Some s -> printf "<details><summary>%s</summary>" s + | _ -> printf "<details>" + + let stop_details () = printf "</details>" + let start_comment () = printf "<span class=\"comment\">(*" let end_comment () = printf "*)</span>" @@ -1053,6 +1064,9 @@ module TeXmacs = struct let start_emph () = printf "<with|font shape|italic|" let stop_emph () = printf ">" + let start_details _ = () + let stop_details () = () + let start_comment () = () let end_comment () = () @@ -1159,6 +1173,9 @@ module Raw = struct let start_emph () = printf "_" let stop_emph () = printf "_" + let start_details _ = () + let stop_details () = () + let start_comment () = printf "(*" let end_comment () = printf "*)" @@ -1272,6 +1289,11 @@ let start_emph = let stop_emph = select Latex.stop_emph Html.stop_emph TeXmacs.stop_emph Raw.stop_emph +let start_details = + select Latex.start_details Html.start_details TeXmacs.start_details Raw.start_details +let stop_details = + select Latex.stop_details Html.stop_details TeXmacs.stop_details Raw.stop_details + let start_latex_math = select Latex.start_latex_math Html.start_latex_math TeXmacs.start_latex_math Raw.start_latex_math let stop_latex_math = diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 485183a4ed..b7a8d4d858 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -29,6 +29,9 @@ val start_module : unit -> unit val start_doc : unit -> unit val end_doc : unit -> unit +val start_details : string option -> unit +val stop_details : unit -> unit + val start_emph : unit -> unit val stop_emph : unit -> unit diff --git a/tools/dune b/tools/dune index c0e4e20f72..d591bb0c37 100644 --- a/tools/dune +++ b/tools/dune @@ -49,8 +49,8 @@ (ocamllex coqwc) (executables - (names coq_tex coq_dune) - (public_names coq-tex coq_dune) + (names coq_tex) + (public_names coq-tex) (package coq) - (modules coq_tex coq_dune) + (modules coq_tex) (libraries str)) |