diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/index.mll | 8 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 20 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 37 |
3 files changed, 36 insertions, 29 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index b41c19ac3..f83b1212e 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -70,12 +70,14 @@ let add_def loc ty sp id = let add_ref m loc m' sp id ty = if Hashtbl.mem reftable (m, loc) then () - else - Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)) + else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty)); + let idx = if id = "<>" then m' else id in + if Hashtbl.mem deftable idx then () + else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty)) let add_mod m loc m' id = Hashtbl.add reftable (m, loc) (Mod (m', id)); - Hashtbl.add deftable id (Mod (m', id)) + Hashtbl.add deftable m (Mod (m', id)) let find m l = Hashtbl.find reftable (m, l) diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 2d547af79..34c993296 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -32,7 +32,7 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; @@ -42,27 +42,31 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Set"; "Types"; "Unset"; "Variable"; "Variables"; "Context"; + "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Boxed"; "Unboxed"; "Inline"; "Arguments"; "Add"; "Strict"; "Typeclasses"; "Instance"; "Class"; "Instantiation"; + "subgoal"; (* Program *) "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma"; "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next"; - "Program Instance"; + "Program Instance"; "Equations"; "Equations_nocomp"; (*i (* coq terms *) *) "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; - "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where" + "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure"; + (* Ltac *) + "before"; "after" ] let is_tactic = build_table - [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite"; - "destruct"; "induction"; "elim"; "dependent"; - "generalize"; "clear"; "rename"; "move"; "set"; "assert"; - "cut"; "assumption"; "exact"; "split"; "try"; "discriminate"; + [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "injection"; + "elimtype"; "progress"; "setoid_rewrite"; + "destruct"; "destruction"; "destruct_call"; "induction"; "elim"; "dependent"; + "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "clear"; "rename"; "move"; "set"; "assert"; + "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; "transitivity"; "replace"; "setoid_replace"; "inversion"; "inversion_clear"; diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index fc40a97c5..d38a09bd6 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -190,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" @@ -226,6 +233,7 @@ let def_token = | "Scheme" | "Inductive" | "CoInductive" + | "Equations" let decl_token = "Hypothesis" @@ -313,12 +321,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 = " " @@ -525,16 +527,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 } | '*'* "*)" |