diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-25 16:27:08 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-25 16:27:08 +0000 |
| commit | 4e1fbaaaf5f8e4988ba4e4e4b49f9dbaf48d2110 (patch) | |
| tree | b2ca3cf1356cd01dbea759aa184f81866242d62e /tools | |
| parent | 2d7da938f00d968399ad1617c7c7147c801315e7 (diff) | |
indexation Record / bug gallina sur := en V8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5382 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
| -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 9525b457e..d12b1fe88 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 0407c3477..bdf48e080 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 | '[' | ']' |