summaryrefslogtreecommitdiff
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll233
1 files changed, 182 insertions, 51 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index a2bcb987..d7b54fd0 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,14 +1,11 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cpretty.mll 14868 2011-12-26 17:07:24Z herbelin $ i*)
-
(*s Utility functions for the scanners *)
{
@@ -80,8 +77,17 @@
let in_proof = ref None
let in_emph = ref false
- let start_emph () = in_emph := true; Output.start_emph ()
- let stop_emph () = if !in_emph then (Output.stop_emph (); in_emph := false)
+ let in_env start stop =
+ let r = ref false in
+ let start_env () = r := true; start () in
+ let stop_env () = if !r then stop (); r := false in
+ (fun x -> !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
@@ -257,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)
}
@@ -323,6 +329,7 @@ let def_token =
| "SubClass"
| "Example"
| "Fixpoint"
+ | "Function"
| "Boxed"
| "CoFixpoint"
| "Record"
@@ -371,13 +378,17 @@ let commands =
| "Drop"
| "ProtectedLoop"
| "Quit"
+ | "Restart"
| "Load"
| "Add"
| "Remove" space+ "Loadpath"
| "Print"
| "Inspect"
| "About"
+ | "SearchAbout"
+ | "SearchRewrite"
| "Search"
+ | "Locate"
| "Eval"
| "Reset"
| "Check"
@@ -405,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"
@@ -412,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 = "*" | "**" | "***" | "****"
@@ -512,7 +532,7 @@ rule coq_bol = parse
output_indented_keyword s lexbuf;
let eol= body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | space* notation_kw space*
+ | space* notation_kw
{ let s = lexeme lexbuf in
output_indented_keyword s lexbuf;
let eol= start_notation_string lexbuf in
@@ -639,7 +659,7 @@ and coq = parse
Output.ident s (lexeme_start lexbuf);
let eol = body lexbuf in
if eol then coq_bol lexbuf else coq lexbuf }
- | notation_kw space*
+ | notation_kw
{ let s = lexeme lexbuf in
Output.ident s (lexeme_start lexbuf);
let eol= start_notation_string lexbuf in
@@ -663,8 +683,6 @@ and coq = parse
(*s Scanning documentation, at beginning of line *)
and doc_bol = parse
- | space* nl+
- { Output.paragraph (); doc_bol lexbuf }
| space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
{ let eol, lex = strip_eol (lexeme lexbuf) in
let lev, s = sec_title lex in
@@ -674,33 +692,26 @@ 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 space* '-'+
- { (* adding this production instead of just letting the paragraph
- production and the begin list production fire eliminates
- extra vertical whitespace. *)
- let buf' = lexeme lexbuf in
- let buf =
- let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
- match bufs with
- | (_ :: s :: []) -> s
- | (_ :: _ :: s :: _) -> s
- | _ -> eprintf "Internal error bad_split1 - please report\n";
- exit 1
+ | 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 buf with
+ match check_start_list line with
| Neither -> backtrack_past_newline lexbuf; doc None lexbuf
- | List n -> Output.item 1; doc (Some [n]) lexbuf
- | Rule -> Output.rule (); doc None lexbuf
- }
- | space* '-'+
- { let buf = lexeme lexbuf in
- match check_start_list buf with
- | Neither -> backtrack lexbuf; doc None lexbuf
- | List n -> Output.item 1; doc (Some [n]) lexbuf
+ | List n -> Output.paragraph ();
+ Output.item 1; doc (Some [n]) lexbuf
| Rule -> Output.rule (); doc None lexbuf
}
+ | 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 }
| '_'
@@ -724,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;
@@ -734,6 +745,8 @@ and doc_list_bol indents = parse
Output.end_inline_coq_block ();
formatted := false;
doc_list_bol indents lexbuf }
+ | "[[[" nl
+ { inf_rules (Some indents) lexbuf }
| space* nl space* '-'
{ (* Like in the doc_bol production, these two productions
exist only to deal properly with whitespace *)
@@ -769,9 +782,16 @@ and doc_list_bol indents = parse
backtrack_past_newline lexbuf;
doc_list_bol indents lexbuf
end
- | Before -> Output.stop_item ();
- backtrack_past_newline lexbuf;
- doc_bol lexbuf
+ | Before ->
+ (* Here we were at the beginning of a line, and it was blank.
+ The next line started before any list items. So: insert
+ a paragraph for the empty line, rewind to whatever's just
+ after the newline, then toss over to doc_bol for whatever
+ comes next. *)
+ Output.stop_item ();
+ Output.paragraph ();
+ backtrack_past_newline lexbuf;
+ doc_bol lexbuf
}
| space* _
@@ -780,7 +800,10 @@ and doc_list_bol indents = parse
| Before -> Output.stop_item (); backtrack lexbuf;
doc_bol lexbuf
| StartLevel n ->
- Output.reach_item_level (n-1);
+ (if n = 1 then
+ Output.stop_item ()
+ else
+ Output.reach_item_level (n-1));
backtrack lexbuf;
doc (Some (take (n-1) indents)) lexbuf
| InLevel (n,_) ->
@@ -808,8 +831,11 @@ and doc indents = parse
| Some ls -> doc_list_bol ls lexbuf
| None -> doc_bol lexbuf
else doc indents lexbuf)}
+ | "[[[" nl
+ { 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;
@@ -823,6 +849,18 @@ and doc indents = parse
let eol = comment lexbuf in
if eol then bol_parse lexbuf else doc indents lexbuf
}
+ | '*'* "*)" space_nl* "(**"
+ {(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 ();
+ doc_bol lexbuf
+ }
| '*'* "*)" space* nl
{ true }
| '*'* "*)"
@@ -857,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 }
| _
@@ -883,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 *)
@@ -911,10 +969,16 @@ and escaped_coq = parse
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
escaped_coq lexbuf }
- | space
- { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
- escaped_coq lexbuf }
- | _
+ | space_nl*
+ { let str = lexeme lexbuf in
+ Tokens.flush_sublexer();
+ (if !Cdglobals.inline_notmono then ()
+ else Output.end_inline_coq ());
+ String.iter Output.char str;
+ (if !Cdglobals.inline_notmono then ()
+ else Output.start_inline_coq ());
+ escaped_coq lexbuf }
+ | _
{ Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
escaped_coq lexbuf }
@@ -1081,7 +1145,7 @@ and body = parse
if eol
then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
else body lexbuf }
- | "where" space*
+ | "where"
{ Tokens.flush_sublexer();
Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
start_notation_string lexbuf }
@@ -1105,6 +1169,8 @@ and body = parse
body lexbuf }
and start_notation_string = parse
+ | space { Tokens.flush_sublexer(); Output.char (lexeme_char lexbuf 0);
+ start_notation_string lexbuf }
| '"' (* a true notation *)
{ Output.sublexer '"' (lexeme_start lexbuf);
notation_string lexbuf;
@@ -1141,6 +1207,71 @@ and printing_token_body = parse
| _ { Buffer.add_string token_buffer (lexeme lexbuf);
printing_token_body lexbuf }
+(*s These handle inference rules, parsing the body segments of things
+ enclosed in [[[ ]]] brackets *)
+and inf_rules indents = parse
+ | space* nl (* blank line, before or between definitions *)
+ { inf_rules indents lexbuf }
+ | "]]]" nl (* end of the inference rules block *)
+ { match indents with
+ | Some ls -> doc_list_bol ls lexbuf
+ | None -> doc_bol lexbuf }
+ | _
+ { backtrack lexbuf; (* anything else must be the first line in a rule *)
+ inf_rules_assumptions indents [] lexbuf}
+
+(* The inference rule parsing just collects the inference rule and then
+ calls the output function once, instead of doing things incrementally
+ like the rest of the lexer. If only there were a real parsing phase...
+*)
+and inf_rules_assumptions indents assumptions = parse
+ | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
+ { let line = lexeme lexbuf in
+ let (spaces,_) = count_spaces line in
+ let dashes_and_name =
+ cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
+ in
+ let ldn = String.length dashes_and_name in
+ let (dashes,name) =
+ try (let i = String.index dashes_and_name ' ' in
+ let d = String.sub dashes_and_name 0 i in
+ let n = cut_head_tail_spaces
+ (String.sub dashes_and_name (i+1) (ldn-i-1))
+ in
+ (d, Some n))
+ with _ -> (dashes_and_name, None)
+
+ in
+ inf_rules_conclusion indents (List.rev assumptions)
+ (spaces, dashes, name) [] lexbuf }
+ | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
+ { let line = lexeme lexbuf in
+ let (spaces,_) = count_spaces line in
+ let assumption = cut_head_tail_spaces
+ (String.sub line 0 (String.length line - 1))
+ in
+ inf_rules_assumptions indents ((spaces,assumption)::assumptions)
+ lexbuf }
+
+(*s The conclusion is required to come immediately after the
+ horizontal bar. It is allowed to contain multiple lines of
+ text, like the assumptions. The conclusion ends when we spot a
+ blank line or a ']]]'. *)
+and inf_rules_conclusion indents assumptions middle conclusions = parse
+ | space* nl | space* "]]]" nl (* end of conclusions. *)
+ { backtrack lexbuf;
+ Output.inf_rule assumptions middle (List.rev conclusions);
+ inf_rules indents lexbuf }
+ | space* [^ '\n']+ nl (* this is a line in the conclusion *)
+ { let line = lexeme lexbuf in
+ let (spaces,_) = count_spaces line in
+ let conc = cut_head_tail_spaces (String.sub line 0
+ (String.length line - 1))
+ in
+ inf_rules_conclusion indents assumptions middle
+ ((spaces,conc) :: conclusions) lexbuf
+ }
+
(*s A small scanner to support the chapter subtitle feature *)
and st_start m = parse
| "(*" "*"+ space+ "*" space+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 13:44:38 +0000