summaryrefslogtreecommitdiff
path: root/tools/coqdoc/pretty.mll
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/pretty.mll')
-rw-r--r--tools/coqdoc/pretty.mll784
1 files changed, 0 insertions, 784 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
deleted file mode 100644
index b29e0734..00000000
--- a/tools/coqdoc/pretty.mll
+++ /dev/null
@@ -1,784 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i $Id: pretty.mll 12908 2010-04-09 08:54:04Z herbelin $ i*)
-
-(*s Utility functions for the scanners *)
-
-{
- open Printf
- open Lexing
-
- (* count the number of spaces at the beginning of a string *)
- let count_spaces s =
- let n = String.length s in
- let rec count c i =
- if i == n then c,i else match s.[i] with
- | '\t' -> count (c + (8 - (c mod 8))) (i + 1)
- | ' ' -> count (c + 1) (i + 1)
- | _ -> c,i
- in
- count 0 0
-
- let count_dashes s =
- let c = ref 0 in
- for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
- !c
-
- let cut_head_tail_spaces s =
- let n = String.length s in
- let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
- let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
- let l = look_up 0 in
- let r = look_dn (n-1) in
- if l <= r then String.sub s l (r-l+1) else s
-
- let sec_title s =
- let rec count lev i =
- if s.[i] = '*' then
- count (succ lev) (succ i)
- else
- let t = String.sub s i (String.length s - i) in
- lev, cut_head_tail_spaces t
- in
- count 0 (String.index s '*')
-
- let strip_eol s =
- let eol = s.[String.length s - 1] = '\n' in
- (eol, if eol then String.sub s 1 (String.length s - 1) else s)
-
-
- let formatted = ref false
- let brackets = ref 0
- let comment_level = ref 0
- let in_proof = ref None
-
- let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
-
- let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
- (* saving/restoring the PP state *)
-
- type state = {
- st_gallina : bool;
- st_light : bool
- }
-
- let state_stack = Stack.create ()
-
- let save_state () =
- Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
-
- let restore_state () =
- let s = Stack.pop state_stack in
- Cdglobals.gallina := s.st_gallina;
- Cdglobals.light := s.st_light
-
- let without_ref r f x = save_state (); r := false; f x; restore_state ()
-
- let without_gallina = without_ref Cdglobals.gallina
-
- let without_light = without_ref Cdglobals.light
-
- let show_all f = without_gallina (without_light f)
-
- let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
- let end_show () = restore_state ()
-
- (* Reset the globals *)
-
- let reset () =
- formatted := false;
- brackets := 0;
- comment_level := 0
-
- (* erasing of Section/End *)
-
- let section_re = Str.regexp "[ \t]*Section"
- let end_re = Str.regexp "[ \t]*End"
- let is_section s = Str.string_match section_re s 0
- let is_end s = Str.string_match end_re s 0
-
- let sections_to_close = ref 0
-
- let section_or_end s =
- if is_section s then begin
- incr sections_to_close; true
- end else if is_end s then begin
- if !sections_to_close > 0 then begin
- decr sections_to_close; true
- end else
- false
- end else
- true
-
- (* tokens pretty-print *)
-
- let token_buffer = Buffer.create 1024
-
- let token_re =
- Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
- let printing_token_re =
- Str.regexp
- "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
-
- let add_printing_token toks pps =
- try
- if Str.string_match token_re toks 0 then
- let tok = Str.matched_group 1 toks in
- if Str.string_match printing_token_re pps 0 then
- let pp =
- (try Some (Str.matched_group 3 pps) with _ ->
- try Some (Str.matched_group 4 pps) with _ -> None),
- (try Some (Str.matched_group 6 pps) with _ -> None)
- in
- Output.add_printing_token tok pp
- with _ ->
- ()
-
- let remove_token_re =
- Str.regexp
- "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
-
- let remove_printing_token toks =
- try
- if Str.string_match remove_token_re toks 0 then
- let tok = Str.matched_group 1 toks in
- Output.remove_printing_token tok
- with _ ->
- ()
-
- let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
- let extract_ident s =
- assert (String.length s >= 3);
- if Str.string_match extract_ident_re s 0 then
- Str.matched_group 1 s
- else
- String.sub s 1 (String.length s - 3)
-
- let symbol lexbuf s = Output.symbol s
-
-}
-
-(*s Regular expressions *)
-
-let space = [' ' '\t']
-let space_nl = [' ' '\t' '\n' '\r']
-let nl = "\r\n" | '\n'
-
-let firstchar =
- ['A'-'Z' 'a'-'z' '_'
- (* iso 8859-1 accents *)
- '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
- (* *)
- '\194' '\185' |
- (* utf-8 latin 1 supplement *)
- '\195' ['\128'-'\191'] |
- (* utf-8 letterlike symbols *)
- '\206' ('\160' | [ '\177'-'\183'] | '\187') |
- '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
- | '\129' [ '\176'-'\187' ] (* superscripts *)
- | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-let identchar =
- firstchar | ['\'' '0'-'9' '@' ]
-let id = firstchar identchar*
-let pfx_id = (id '.')*
-let identifier =
- id | pfx_id id
-
-let symbolchar_symbol_no_brackets =
- ['!' '$' '%' '&' '*' '+' ',' '^' '#'
- '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
- (* utf-8 symbols *)
- '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
-let symbolchar_no_brackets = symbolchar_symbol_no_brackets |
- [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
-let symbolchar = symbolchar_no_brackets | '[' | ']'
-let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
-let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
-let printing_token = (token | id)+
-
-(* tokens with balanced brackets *)
-let token_brackets =
- ( token_no_brackets ('[' token_no_brackets? ']')*
- | token_no_brackets? ('[' token_no_brackets? ']')+ )
- token_no_brackets?
-
-let thm_token =
- "Theorem"
- | "Lemma"
- | "Fact"
- | "Remark"
- | "Corollary"
- | "Proposition"
- | "Property"
- | "Goal"
-
-let prf_token =
- "Next" space+ "Obligation"
- | "Proof" (space* "." | space+ "with")
-
-let def_token =
- "Definition"
- | "Let"
- | "Class"
- | "SubClass"
- | "Example"
- | "Local"
- | "Fixpoint"
- | "Boxed"
- | "CoFixpoint"
- | "Record"
- | "Structure"
- | "Scheme"
- | "Inductive"
- | "CoInductive"
- | "Equations"
- | "Instance"
- | "Global" space+ "Instance"
-
-let decl_token =
- "Hypothesis"
- | "Hypotheses"
- | "Parameter"
- | "Axiom" 's'?
- | "Conjecture"
-
-let gallina_ext =
- "Module"
- | "Include" space+ "Type"
- | "Include"
- | "Declare" space+ "Module"
- | "Transparent"
- | "Opaque"
- | "Canonical"
- | "Coercion"
- | "Identity"
- | "Implicit"
- | "Notation"
- | "Infix"
- | "Tactic" space+ "Notation"
- | "Reserved" space+ "Notation"
- | "Section"
- | "Context"
- | "Variable" 's'?
- | ("Hypothesis" | "Hypotheses")
- | "End"
-
-let commands =
- "Pwd"
- | "Cd"
- | "Drop"
- | "ProtectedLoop"
- | "Quit"
- | "Load"
- | "Add"
- | "Remove" space+ "Loadpath"
- | "Print"
- | "Inspect"
- | "About"
- | "Search"
- | "Eval"
- | "Reset"
- | "Check"
- | "Type"
-
- | "Section"
- | "Chapter"
- | "Variable" 's'?
- | ("Hypothesis" | "Hypotheses")
- | "End"
-
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
-
-let extraction =
- "Extraction"
- | "Recursive" space+ "Extraction"
- | "Extract"
-
-let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
-
-let prog_kw =
- "Program" space+ gallina_kw
- | "Obligation"
- | "Obligations"
- | "Solve"
-
-let gallina_kw_to_hide =
- "Implicit" space+ "Arguments"
- | "Ltac"
- | "Require"
- | "Import"
- | "Export"
- | "Load"
- | "Hint"
- | "Open"
- | "Close"
- | "Delimit"
- | "Transparent"
- | "Opaque"
- | ("Declare" space+ ("Morphism" | "Step") )
- | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
- | "Declare" space+ ("Left" | "Right") space+ "Step"
-
-
-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_verb = "(*" space* "begin" space+ "verb" space* "*)"
-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)) then Output.empty_line_of_code (); coq_bol lexbuf }
- | space* "(**" space_nl
- { 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* gallina_kw_to_hide
- { let s = lexeme lexbuf in
- if !Cdglobals.light && section_or_end s then
- let eol = skip_to_dot lexbuf in
- if eol then (coq_bol lexbuf) else coq lexbuf
- else
- begin
- 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);
- let eol = body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end }
- | space* thm_token
- { let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- let s = String.sub s isp (String.length s - isp) in
- Output.indentation nbsp;
- Output.ident s (lexeme_start lexbuf + isp);
- let eol = body lexbuf in
- in_proof := Some eol;
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* prf_token
- { in_proof := Some true;
- let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- let s = lexeme lexbuf in
- if s.[String.length s - 1] = '.' then false
- else skip_to_dot lexbuf
- in if eol then coq_bol lexbuf else coq lexbuf }
- | space* end_kw {
- let eol =
- if not (!in_proof <> None && !Cdglobals.gallina) then
- begin backtrack lexbuf; body_bol lexbuf end
- else skip_to_dot lexbuf
- in
- in_proof := None;
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* gallina_kw
- {
- in_proof := None;
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- let s = String.sub s isp (String.length s - isp) in
- Output.indentation nbsp;
- Output.ident s (lexeme_start lexbuf + isp);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | space* prog_kw
- {
- in_proof := None;
- let s = lexeme lexbuf in
- 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);
- let eol= body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
-
- | space* "(**" space+ "printing" space+ printing_token space+
- { let tok = lexeme lexbuf in
- let s = printing_token_body lexbuf in
- add_printing_token tok s;
- coq_bol lexbuf }
- | space* "(**" space+ "printing" space+
- { eprintf "warning: bad 'printing' command at character %d\n"
- (lexeme_start lexbuf); flush stderr;
- comment_level := 1;
- ignore (comment lexbuf);
- coq_bol lexbuf }
- | space* "(**" space+ "remove" space+ "printing" space+
- (identifier | token) space* "*)"
- { remove_printing_token (lexeme lexbuf);
- coq_bol lexbuf }
- | space* "(**" space+ "remove" space+ "printing" space+
- { eprintf "warning: bad 'remove printing' command at character %d\n"
- (lexeme_start lexbuf); flush stderr;
- comment_level := 1;
- ignore (comment lexbuf);
- coq_bol lexbuf }
- | space* "(*"
- { comment_level := 1;
- if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- Output.start_comment ();
- end;
- let eol = comment lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | eof
- { () }
- | _
- { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- skip_to_dot lexbuf
- in
- if eol then coq_bol lexbuf else coq lexbuf }
-
-(*s Scanning Coq elsewhere *)
-
-and coq = parse
- | nl
- { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
- | "(**" space_nl
- { 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 }
- | "(*"
- { comment_level := 1;
- if !Cdglobals.parse_comments then begin
- let s = lexeme lexbuf in
- let nbsp,isp = count_spaces s in
- Output.indentation nbsp;
- Output.start_comment ();
- end;
- let eol = comment lexbuf in
- if eol then coq_bol lexbuf
- else coq lexbuf
- }
- | nl+ space* "]]"
- { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
- | eof
- { () }
- | gallina_kw_to_hide
- { let s = lexeme lexbuf in
- if !Cdglobals.light && section_or_end s then
- begin
- let eol = skip_to_dot lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end
- else
- begin
- Output.ident s (lexeme_start lexbuf);
- let eol=body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf
- end }
- | prf_token
- { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body_bol lexbuf end
- else
- let s = lexeme lexbuf in
- let eol =
- if s.[String.length s - 1] = '.' then false
- else skip_to_dot lexbuf
- in
- eol
- in if eol then coq_bol lexbuf else coq lexbuf }
- | end_kw {
- let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body lexbuf end
- else
- let eol = skip_to_dot lexbuf in
- if !in_proof <> Some true && eol then
- Output.line_break ();
- eol
- in
- in_proof := None;
- if eol then coq_bol lexbuf else coq lexbuf }
- | gallina_kw
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
- let eol = body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | prog_kw
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
- let eol = body lexbuf in
- if eol then coq_bol lexbuf else coq lexbuf }
- | space+ { Output.char ' '; coq lexbuf }
- | eof
- { () }
- | _ { let eol =
- if not !Cdglobals.gallina then
- begin backtrack lexbuf; body lexbuf end
- else
- skip_to_dot lexbuf
- in
- if eol then coq_bol lexbuf else coq lexbuf}
-
-(*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
- Output.section lev (fun () -> ignore (doc (from_string s)));
- if eol then doc_bol lexbuf else doc lexbuf }
- | space* '-'+
- { let n = count_dashes (lexeme lexbuf) in
- if n >= 4 then Output.rule () else Output.item n;
- doc lexbuf }
- | "<<" space*
- { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
- | eof
- { true }
- | _
- { backtrack lexbuf; doc lexbuf }
-
-(*s Scanning documentation elsewhere *)
-
-and doc = parse
- | nl
- { Output.char '\n'; doc_bol lexbuf }
- | "[[" nl
- { formatted := true; Output.line_break (); Output.start_inline_coq ();
- let eol = body_bol lexbuf in
- Output.end_inline_coq (); formatted := false;
- if eol then doc_bol lexbuf else doc lexbuf}
- | "["
- { brackets := 1;
- Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
- doc lexbuf }
- | '*'* "*)" space* nl
- { true }
- | '*'* "*)"
- { false }
- | "$"
- { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
- | "$$"
- { Output.char '$'; doc lexbuf }
- | "%"
- { escaped_latex lexbuf; doc lexbuf }
- | "%%"
- { Output.char '%'; doc lexbuf }
- | "#"
- { escaped_html lexbuf; doc lexbuf }
- | "##"
- { Output.char '#'; doc lexbuf }
- | eof
- { false }
- | _
- { Output.char (lexeme_char lexbuf 0); doc lexbuf }
-
-(*s Various escapings *)
-
-and escaped_math_latex = parse
- | "$" { Output.stop_latex_math () }
- | eof { Output.stop_latex_math () }
- | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
-
-and escaped_latex = parse
- | "%" { () }
- | eof { () }
- | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
-
-and escaped_html = parse
- | "#" { () }
- | "&#"
- { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
- | "##"
- { Output.html_char '#'; escaped_html lexbuf }
- | eof { () }
- | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
-
-and verbatim = parse
- | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
- | eof { Output.stop_verbatim () }
- | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
-
-(*s Coq, inside quotations *)
-
-and escaped_coq = parse
- | "]"
- { decr brackets;
- if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
- | "["
- { incr brackets; Output.char '['; escaped_coq lexbuf }
- | "(*"
- { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
- | "*)"
- { (* likely to be a syntax error: we escape *) backtrack lexbuf }
- | eof
- { () }
- | token_brackets
- { let s = lexeme lexbuf in
- symbol lexbuf s; escaped_coq lexbuf }
- | (identifier '.')* identifier
- { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
- | _
- { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
-
-(*s Coq "Comments" command. *)
-
-and comments = parse
- | space_nl+
- { Output.char ' '; comments lexbuf }
- | '"' [^ '"']* '"'
- { let s = lexeme lexbuf in
- let s = String.sub s 1 (String.length s - 2) in
- ignore (doc (from_string s)); comments lexbuf }
- | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
- { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
- | "." (space_nl | eof)
- { () }
- | eof
- { () }
- | _
- { Output.char (lexeme_char lexbuf 0); comments lexbuf }
-
-(*s Skip comments *)
-
-and comment = parse
- | "(*" { incr comment_level;
- if !Cdglobals.parse_comments then Output.start_comment ();
- comment lexbuf }
- | "*)" space* nl {
- if !Cdglobals.parse_comments then (Output.end_comment (); Output.line_break ());
- decr comment_level; if !comment_level > 0 then comment lexbuf else true }
- | "*)" {
- if !Cdglobals.parse_comments then (Output.end_comment ());
- decr comment_level; if !comment_level > 0 then comment lexbuf else false }
- | "[" {
- if !Cdglobals.parse_comments then (
- brackets := 1;
- Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ());
- comment lexbuf }
- | eof { false }
- | space+ { if !Cdglobals.parse_comments then
- Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
- | nl { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
- | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
- comment lexbuf }
-
-and skip_to_dot = parse
- | '.' space* nl { true }
- | eof | '.' space+ { false }
- | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
- | _ { skip_to_dot lexbuf }
-
-and body_bol = parse
- | space+
- { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
- | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
-
-and body = parse
- | nl {Output.line_break(); body_bol lexbuf}
- | nl+ space* "]]"
- { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
- | eof { false }
- | '.' space* nl | '.' space* eof
- { Output.char '.'; Output.line_break();
- if not !formatted then true else body_bol lexbuf }
- | '.' space+ { Output.char '.'; Output.char ' ';
- if not !formatted then false else body lexbuf }
- | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
- | "(*" { comment_level := 1;
- if !Cdglobals.parse_comments then Output.start_comment ();
- let eol = comment lexbuf in
- if eol
- then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end
- else body lexbuf }
- | identifier
- { let s = lexeme lexbuf in
- Output.ident s (lexeme_start lexbuf);
- body lexbuf }
- | token_no_brackets
- { let s = lexeme lexbuf in
- symbol lexbuf s; body lexbuf }
- | ".."
- { Output.char '.'; Output.char '.';
- body lexbuf }
- | _ { let c = lexeme_char lexbuf 0 in
- Output.char c;
- body lexbuf }
-
-and notation_bol = parse
- | space+
- { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
- | _ { backtrack lexbuf; notation lexbuf }
-
-and notation = parse
- | nl { Output.line_break(); notation_bol lexbuf }
- | '"' { Output.char '"'}
- | token
- { let s = lexeme lexbuf in
- symbol lexbuf s; notation lexbuf }
- | _ { let c = lexeme_char lexbuf 0 in
- Output.char c;
- notation lexbuf }
-
-and skip_hide = parse
- | eof | end_hide { () }
- | _ { skip_hide lexbuf }
-
-(*s Reading token pretty-print *)
-
-and printing_token_body = parse
- | "*)" nl? | eof
- { let s = Buffer.contents token_buffer in
- Buffer.clear token_buffer;
- s }
- | _ { Buffer.add_string token_buffer (lexeme lexbuf);
- printing_token_body lexbuf }
-
-(*s Applying the scanners to files *)
-
-{
-
- let coq_file f m =
- reset ();
- Index.current_library := m;
- Output.start_module ();
- let c = open_in f in
- let lb = from_channel c in
- Output.start_coq (); coq_bol lb; Output.end_coq ();
- close_in c
-
-}
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 11:21:48 +0000