From 4e1fbaaaf5f8e4988ba4e4e4b49f9dbaf48d2110 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 25 Feb 2004 16:27:08 +0000
Subject: 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
---
 tools/coqdoc/index.mll  | 2 ++
 tools/coqdoc/pretty.mll | 8 ++++++--
 2 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'tools')

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 | '[' | ']'
-- 
cgit v1.2.3