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

[helm.git] / matitaB / components / content / notationEnv.ml

diff --git a/matitaB/components/content/notationEnv.ml b/matitaB/components/content/notationEnv.ml
index be9171a8d9318a714e16fd5ceffbc2a069099278..eb85ec038a2623127c69d2414708d8893f94a2a3 100644 (file)
--- a/matitaB/components/content/notationEnv.ml
+++ b/matitaB/components/content/notationEnv.ml
@@ -32,18 +32,20 @@ type ident_or_var =
  | Var of string
 
 type value =
-  | TermValue of Ast.term
+  | TermValue of NotationPt.term
   | StringValue of ident_or_var
   | NumValue of string
   | OptValue of value option
   | ListValue of value list
+  | DisambiguationValue of (Stdpp.location * string option * string option)
 
 type value_type =
-  | TermType of int
+  | TermType of int (* the level of the expected term *)
   | StringType
   | NumType
   | OptType of value_type
   | ListType of value_type
+  | NoType
 
 exception Value_not_found of string
 exception Type_mismatch of string * value_type
@@ -52,6 +54,21 @@ type declaration = string * value_type
 type binding = string * (value_type * value)
 type t = binding list
 
+(* let rec pp_value = function
+ | TermValue t -> "T#" ^ NotationPp.pp_term (new NCicPp.status) t
+ | StringValue (Ident i) -> "I#" ^ i
+ | StringValue (Var v) -> "V#" ^ v
+ | NumValue n -> "N#" ^ n
+ | OptValue None -> "O#None"
+ | OptValue (Some v) -> "O#" ^ pp_value v
+ | ListValue vl -> "L#[" ^ (String.concat ";" (List.map pp_value vl)) ^ "]"
+ | DisambiguationValue _ -> "D#"
+
+let pp_binding = function
+ | s, (ty,v) -> Printf.sprintf "{ %s := %s : %s }" s (pp_value v) "..."
+
+let pp_env e = String.concat " " (List.map pp_binding e) *)
+
 let lookup env name =
   try
     List.assoc name env
@@ -107,12 +124,12 @@ let declaration_of_var = function
 
 let value_of_term = function
   | Ast.Num (s, _) -> NumValue s
-  | Ast.Ident (s, None) -> StringValue (Var s)
+  | Ast.Ident (s, (* `Ambiguous? *) _) -> StringValue (Var s)
   | t -> TermValue t
 
 let term_of_value = function
-  | NumValue s -> Ast.Num (s, 0)
-  | StringValue (Ident s) -> Ast.Ident (s, None)
+  | NumValue s -> Ast.Num (s, None)
+  | StringValue (Ident s) -> Ast.Ident (s, `Ambiguous)
   | TermValue t -> t
   | _ -> assert false (* TO BE UNDERSTOOD *)