First commit with new (incomplete) disambiguation engine.

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

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 6846c30b5b9e608fe96af08fbb60b740ccf24b19..7473838ca5e6b6424e36017dc08b1c28cebe7c09 100644 (file)
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -75,7 +75,8 @@ let number s =
     (Ast.Literal (`Number s))
 
 let ident i =
-  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) 
+    (Ast.Ident (i,`Ambiguous))
 
 let ident_w_href href i =
   match href with
@@ -89,7 +90,7 @@ let binder_symbol s =
     (builtin_symbol s)
 
 let xml_of_sort x = 
-  let to_string x = Ast.Ident (x, None) in
+  let to_string x = Ast.Ident (x, `Ambiguous) in
   let identify x = 
     add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
   in
@@ -271,8 +272,7 @@ let pp_ast0 status t k =
     | Ast.Sort sort -> aux_sort sort
     | Ast.Num _
     | Ast.Symbol _
-    | Ast.Ident (_, None) | Ast.Ident (_, Some [])
-    | Ast.Uri (_, None) | Ast.Uri (_, Some [])
+    | Ast.Ident _ 
     | Ast.Literal _
     | Ast.UserInput as leaf -> leaf
     | t -> NotationUtil.visit_ast ~special_k k t
@@ -599,11 +599,6 @@ let instantiate_level2 status env term =
     | Ast.LetRec (kind, definitions, body) ->
         Ast.LetRec (kind, List.map (aux_definition env) definitions,
           aux env body)
-    | Ast.Uri (name, None) -> Ast.Uri (name, None)
-    | Ast.Uri (name, Some substs) ->
-        Ast.Uri (name, Some (aux_substs env substs))
-    | Ast.Ident (name, Some substs) ->
-        Ast.Ident (name, Some (aux_substs env substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 
     | Ast.Implicit _
@@ -636,14 +631,14 @@ let instantiate_level2 status env term =
     List.map (fun (name, term) -> (name, aux env term)) substs
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
-    | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
+    | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, None)
     | Ast.IdentVar name ->
        (match Env.lookup_string env name with
-           Env.Ident x -> Ast.Ident (x, None)
+           Env.Ident x -> Ast.Ident (x, `Ambiguous)
          | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
-    | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
+    | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, `Ambiguous)
     | Ast.Ascription (term, name) -> assert false
   and aux_magic env = function
     | Ast.Default (some_pattern, none_pattern) ->