lexer updated with the new reference syntax +

[helm.git] / matita / components / content_pres / cicNotationLexer.ml

diff --git a/matita/components/content_pres/cicNotationLexer.ml b/matita/components/content_pres/cicNotationLexer.ml
index eaabf61e7a483d684bf327d912e84c33098507b3..d86a3124d67608b9791c0b122eaa3cf2e1c0cf92 100644 (file)
--- a/matita/components/content_pres/cicNotationLexer.ml
+++ b/matita/components/content_pres/cicNotationLexer.ml
@@ -137,13 +137,14 @@ let regexp uri =
 let regexp nreference =
   "cic:/"                             (* schema *)
   uri_step ('/' uri_step)*            (* path *)
-  '.'
+  '#'
   ( "dec"
-  | "def" "(" number ")"
-  | "fix" "(" number "," number "," number ")"
-  | "cfx" "(" number ")"
-  | "ind" "(" number "," number "," number ")"
-  | "con" "(" number "," number "," number ")") (* ext + reference *)
+  | "def" ":" number ""
+  | "fix" ":" number ":" number ":" number
+  | "cfx" ":" number
+  | "ind" ":" number ":" number ":" number
+  | "con" ":" number ":" number ":" number
+  ) (* ext + reference *)
 
 let error lexbuf msg =
   let begin_cnum, end_cnum = Ulexing.loc lexbuf in