Added support for hyperlinks in the goal view of the web interface.

[helm.git] / matitaB / components / content_pres / cicNotationParser.ml

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 82037a1d6a69e8452a194e668eebfc2f1f348b8a..7361bf59993f7394d31fbb5c4ba7f19c4d46c834 100644 (file)
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -157,9 +157,9 @@ let gram_term status = function
 
 let gram_of_literal status =
   function
-  | `Symbol s -> gram_symbol status s
-  | `Keyword s -> gram_keyword s
-  | `Number s -> gram_number s
+  | `Symbol (s,_) -> gram_symbol status s
+  | `Keyword (s,_) -> gram_keyword s
+  | `Number (s,_) -> gram_number s
 
 let make_action status action bindings =
   let rec aux (vl : NotationEnv.t) =
@@ -226,9 +226,9 @@ let update_sym_grammar status pattern =
         assert false
   and aux_literal status =
     function
-    | `Symbol s -> add_symbol_to_grammar status s
-    | `Keyword s -> status
-    | `Number s -> status
+    | `Symbol (s,_) -> add_symbol_to_grammar status s
+    | `Keyword _ -> status
+    | `Number _ -> status
   and aux_layout status = function
     | Ast.Sub (p1, p2) -> aux (aux status p1) p2
     | Ast.Sup (p1, p2) -> aux (aux status p1) p2
@@ -273,11 +273,11 @@ let extract_term_production status pattern =
         assert false
   and aux_literal =
     function
-    | `Symbol s -> [NoBinding, gram_symbol status s]
-    | `Keyword s ->
+    | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
+    | `Keyword (s,_) ->
         (* assumption: s will be registered as a keyword with the lexer *)
         [NoBinding, gram_keyword s]
-    | `Number s -> [NoBinding, gram_number s]
+    | `Number (s,_) -> [NoBinding, gram_number s]
   and aux_layout = function
     | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
     | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
@@ -528,9 +528,9 @@ EXTEND
         fun l -> List.map (fun x -> x l) p ] 
   ];
   literal: [
-    [ s = SYMBOL -> `Symbol s
-    | k = QKEYWORD -> `Keyword k
-    | n = NUMBER -> `Number n
+    [ s = SYMBOL -> `Symbol (s, (None,None))
+    | k = QKEYWORD -> `Keyword (k, (None,None))
+    | n = NUMBER -> `Number (n,(None,None))
     ]
   ];
   sep:       [ [ "sep";      sep = literal -> sep ] ];