diff options
| -rw-r--r-- | tools/coqdoc/index.mll | 2 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 8 |
2 files changed, 8 insertions, 2 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 9525b457e0..d12b1fe88e 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -189,6 +189,8 @@ rule traverse = parse | "Inductive" space { current_type := Inductive; index_ident lexbuf; inductive lexbuf; traverse lexbuf } + | "Record" space + { current_type := Inductive; index_ident lexbuf; traverse lexbuf } | "Module" (space+ "Type")? space { current_type := Module; index_ident lexbuf; traverse lexbuf } (*i*** diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 0407c3477a..bdf48e0803 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -63,6 +63,7 @@ type gallina_state = Nothing | AfterDot | Proof let gstate = ref AfterDot + let gparen = ref 0 let is_proof = let t = Hashtbl.create 13 in @@ -77,7 +78,10 @@ if id <> "Add" then gstate := Nothing let gallina_symbol s = - if !gstate = AfterDot || (!gstate = Proof && s = ":=") then + if s = "(" then incr gparen + else if s = ")" then decr gparen + else if !gstate = AfterDot || + (!gstate = Proof && !gparen = 0 && s = ":=") then gstate := Nothing let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false @@ -202,7 +206,7 @@ let identifier = firstchar identchar* let symbolchar_no_brackets = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#' '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' - '{' '}'] | + '{' '}' '(' ')'] | (* utf-8 symbols *) '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _ let symbolchar = symbolchar_no_brackets | '[' | ']' |