diff options
Diffstat (limited to 'tools/coqdoc/pretty.mll')
| -rw-r--r-- | tools/coqdoc/pretty.mll | 113 |
1 files changed, 80 insertions, 33 deletions
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index baace5ba..3ae5cbed 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 11255 2008-07-24 16:57:13Z notin $ i*) +(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*) (*s Utility functions for the scanners *) @@ -57,6 +57,7 @@ let formatted = ref false let brackets = ref 0 let comment_level = ref 0 + let in_proof = ref false let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos @@ -173,11 +174,12 @@ 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' ['\177'-'\183'] | + '\206' ('\160' | [ '\177'-'\183'] | '\187') | '\226' ('\130' [ '\128'-'\137' ] (* subscripts *) | '\129' [ '\176'-'\187' ] (* superscripts *) | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143']) @@ -188,17 +190,24 @@ let pfx_id = (id '.')* let identifier = id | pfx_id id -let symbolchar_no_brackets = - ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' - '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' - '{' '}' '(' ')'] | +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_no_brackets+ -let token = symbolchar+ | '[' [^ '[' ']' ':']* ']' +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" @@ -208,22 +217,26 @@ let thm_token = | "Proposition" | "Property" | "Goal" + | "Next" space+ "Obligation" let def_token = "Definition" | "Let" | "Class" - | "SubClass" + | "SubClass" | "Example" | "Local" | "Fixpoint" + | "Boxed" | "CoFixpoint" | "Record" | "Structure" - | "Instance" | "Scheme" | "Inductive" | "CoInductive" + | "Equations" + | "Instance" + | "Global" space+ "Instance" let decl_token = "Hypothesis" @@ -277,6 +290,8 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" +let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort" + let extraction = "Extraction" | "Recursive" space+ "Extraction" @@ -291,7 +306,8 @@ let prog_kw = | "Solve" let gallina_kw_to_hide = - "Implicit" + "Implicit" space+ "Arguments" + | "Next" "Obligation" | "Ltac" | "Require" | "Import" @@ -308,12 +324,6 @@ let gallina_kw_to_hide = | "Declare" space+ ("Left" | "Right") space+ "Step" -(* tokens with balanced brackets *) -let token_brackets = - ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* - | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ ) - symbolchar_no_brackets* - let section = "*" | "**" | "***" | "****" let item_space = " " @@ -333,7 +343,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" rule coq_bol = parse | space* nl+ - { Output.empty_line_of_code (); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf } | space* "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -352,7 +362,7 @@ rule coq_bol = parse { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then let eol = skip_to_dot lexbuf in - if eol then (Output.line_break (); coq_bol lexbuf) else coq lexbuf + if eol then (coq_bol lexbuf) else coq lexbuf else begin let nbsp,isp = count_spaces s in @@ -362,16 +372,45 @@ rule coq_bol = parse let eol = body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } - | space* gallina_kw + | 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 := true; + if eol then coq_bol lexbuf else coq lexbuf } + | space* "Proof" (space* "." | space+ "with") + { in_proof := true; + let eol = + if not !Cdglobals.gallina then + begin backtrack lexbuf; body_bol lexbuf end + else true + in if eol then coq_bol lexbuf else coq lexbuf } + | space* end_kw { + let eol = + if not (!in_proof && !Cdglobals.gallina) then + begin backtrack lexbuf; body_bol lexbuf end + else + skip_to_dot lexbuf + in + in_proof := false; + if eol then coq_bol lexbuf else coq lexbuf } + | space* gallina_kw + { + in_proof := false; + 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 - { let s = lexeme lexbuf in + { + in_proof := false; + 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 @@ -409,7 +448,7 @@ rule coq_bol = parse | _ { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body_bol lexbuf end + begin backtrack lexbuf; body_bol lexbuf end else skip_to_dot lexbuf in @@ -419,7 +458,7 @@ rule coq_bol = parse and coq = parse | nl - { Output.line_break(); coq_bol lexbuf } + { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf } | "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -448,6 +487,15 @@ and coq = parse let eol=body lexbuf in if eol then coq_bol lexbuf else coq lexbuf end } + | end_kw { + let eol = + if not (!in_proof && !Cdglobals.gallina) then + begin backtrack lexbuf; body lexbuf end + else + skip_to_dot lexbuf + in + in_proof := false; + if eol then coq_bol lexbuf else coq lexbuf } | gallina_kw { let s = lexeme lexbuf in Output.ident s (lexeme_start lexbuf); @@ -463,7 +511,7 @@ and coq = parse { () } | _ { let eol = if not !Cdglobals.gallina then - begin backtrack lexbuf; Output.indentation 0; body lexbuf end + begin backtrack lexbuf; body lexbuf end else let eol = skip_to_dot lexbuf in if eol then Output.line_break (); eol @@ -496,16 +544,15 @@ and doc_bol = parse and doc = parse | nl { Output.char '\n'; doc_bol lexbuf } - | "[" - { brackets := 1; - Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq (); - doc lexbuf } - | "[[" nl space* + | "[[" nl { formatted := true; Output.line_break (); Output.start_inline_coq (); - Output.indentation (fst (count_spaces (lexeme lexbuf))); 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 } | '*'* "*)" @@ -612,7 +659,7 @@ and skip_to_dot = parse and body_bol = parse | space+ { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf } - | _ { backtrack lexbuf; body lexbuf } + | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } and body = parse | nl {Output.line_break(); body_bol lexbuf} @@ -645,7 +692,7 @@ and notation_bol = parse and notation = parse | nl { Output.line_break(); notation_bol lexbuf } - | '"' { Output.char '"'; false } + | '"' { Output.char '"'} | token { let s = lexeme lexbuf in Output.symbol s; notation lexbuf } @@ -660,7 +707,7 @@ and skip_hide = parse (*s Reading token pretty-print *) and printing_token_body = parse - | "*)" | eof + | "*)" nl? | eof { let s = Buffer.contents token_buffer in Buffer.clear token_buffer; s } |