textual parser fixed

diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
index 31878bfe6e83d68405f1759597f7d5ac5840d4d4..1be084795a11505eb80764da93da88e1ad79d5b6 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
+++ b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll
@@ -49,7 +49,7 @@
  ;;
 }
 let num = ['1'-'9']['0'-'9']* | '0'
-let alfa = ['A'-'Z' 'a'-'z' '_']
+let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-']
 let ident = alfa (alfa | num)*
 let baseuri = '/'(ident '/')* ident '.'
 let conuri = baseuri ("con" | "var")

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index b85be0754e7194cd9efc140d365d4295339915c6..af67f1c1454a8a367ef033b3034e1275b4be7aa0 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -123,7 +123,9 @@ expr2:
         Hashtbl.find uri_of_id_map $1
        with
         Not_found ->
-         raise (UnknownIdentifier $1)
+        match ! CicTextualParser0.locate_object $1 with
+         | None      -> raise (UnknownIdentifier $1)
+         | Some term -> Hashtbl.add uri_of_id_map $1 term; term  
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let cookingno = get_cookingno (fst $5) in

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
index 0a841473474275adee71d1b89f11a3f8b47eeaf5..fe4bf062346c95b9cf29eaeb692871f4fccab3fd 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser0.ml
@@ -28,3 +28,7 @@ exception Eof;;
 let current_uri = ref (UriManager.uri_of_string "cic:/dummy.con");;
 let binders = ref ([] : (Cic.name option) list);;
 let metasenv = ref ([] : Cic.metasenv);;
+let locate_object = ref ((fun _ -> None):string->Cic.term option);;
+
+let set_locate_object f =
+   locate_object := f

diff --git a/helm/ocaml/mathql/.depend b/helm/ocaml/mathql/.depend
index 0d8aa0719c2a11d08b9ba944ae0b29c14a36ee88..c898ba8b0aa6f3c42389bf24244818592d9dae2c 100644 (file)
--- a/helm/ocaml/mathql/.depend
+++ b/helm/ocaml/mathql/.depend
@@ -2,7 +2,9 @@ mQueryTParser.cmi: mathQL.cmo
 mQueryUtil.cmi: mathQL.cmo 
 mQueryTParser.cmo: mathQL.cmo mQueryTParser.cmi 
 mQueryTParser.cmx: mathQL.cmx mQueryTParser.cmi 
-mQueryUtil.cmo: mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo mQueryUtil.cmi 
-mQueryUtil.cmx: mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx mQueryUtil.cmi 
 mQueryTLexer.cmo: mQueryTParser.cmi 
 mQueryTLexer.cmx: mQueryTParser.cmx 
+mQueryUtil.cmo: mQueryHTML.cmo mQueryTLexer.cmo mQueryTParser.cmi mathQL.cmo \
+    mQueryUtil.cmi 
+mQueryUtil.cmx: mQueryHTML.cmx mQueryTLexer.cmx mQueryTParser.cmx mathQL.cmx \
+    mQueryUtil.cmi 

diff --git a/helm/ocaml/mathql/Makefile b/helm/ocaml/mathql/Makefile
index f9c0eb9d8f8e419b605eca06fed9316e24408025..8cd40ee82dee8c5d186168e934261d568d49ce74 100644 (file)
--- a/helm/ocaml/mathql/Makefile
+++ b/helm/ocaml/mathql/Makefile
@@ -5,10 +5,11 @@ PREDICATES =
 INTERFACE_FILES = mQueryTParser.mli mQueryUtil.mli
 
 IMPLEMENTATION_FILES = mathQL.ml mQueryTParser.ml mQueryTLexer.ml \
-                      mQueryUtil.ml
+                      mQueryHTML.ml mQueryUtil.ml
 
 EXTRA_OBJECTS_TO_INSTALL = mathQL.ml mathQL.cmi mQueryTLexer.cmi \
-                          mQueryTLexer.mll mQueryTParser.mly
+                          mQueryTLexer.mll mQueryTParser.mly \
+                           mQueryHTML.ml mQueryHTML.cmi 
 
 EXTRA_OBJECTS_TO_CLEAN = mQueryTParser.ml mQueryTParser.mli \
                          mQueryTLexer.ml

diff --git a/helm/ocaml/mathql/mQueryUtil.ml b/helm/ocaml/mathql/mQueryUtil.ml
index 0cf8ebe087653b2d4365c0e33628fafa7a1049eb..8943e5675652f23f2b60c64b92c902575a8d4652 100644 (file)
--- a/helm/ocaml/mathql/mQueryUtil.ml
+++ b/helm/ocaml/mathql/mQueryUtil.ml
@@ -34,8 +34,9 @@
 (******************************************************************************)
 
 open MathQL
+open MQueryHTML
 
-(* string linearization of a reference *)
+(* string linearization of a reference **************************************)
 
 let str_btoken = function
    | MQBC s -> s
@@ -75,29 +76,7 @@ let str_uref (u, i) =
 let xp_str_uref (u, i) =
    UriManager.string_of_uri u ^ str_frag true string_of_int i
 
-(* raw HTML representation *)
-
-let key s = "<font color=\"blue\">" ^ s ^ " </font>"
-
-let sub s = "<font color=\"blue\"> " ^ s ^ " </font>"
-
-let sub2 s = "<font color=\"blue\">" ^ s ^ "</font>"
-
-let sym s = s
-
-let sep s = s
-
-let str s = "<font color=\"red\">'" ^ s ^ "'</font>"
-
-let pat s = "<font color=\"red\">\"" ^ s ^ "\"</font>"
-
-let res s = "<font color=\"brown\">\"" ^ s ^ "\"</font>"
-
-let nl () = "<br>"
-
-let par () = "<p>"
-
-(* HTML representation of a query *)
+(* HTML representation of a query ********************************************)
 
 let out_rvar s = sym s
 
@@ -110,7 +89,7 @@ let out_tref r = pat (str_tref r)
 let rec out_sequence f = function
   | []        -> sep "."
   | [s]       -> f s
-  | s :: tail -> f s ^ sep "," ^ out_sequence f tail
+  | s :: tail -> f s ^ sep ", " ^ out_sequence f tail
 
 let out_order = function
    | MQAsc  -> sub2 "asc"
@@ -175,7 +154,7 @@ and out_list = function
 let out_query = function
    | MQList l -> out_list l
 
-(* HTML representation of a query result *)
+(* HTML representation of a query result ************************************)
 
 let rec out_res_list = function 
    | []     -> ""
@@ -186,7 +165,7 @@ let out_result qr =
    match qr with
       | MQRefs l -> out_res_list l
 
-(* Converting functions *)
+(* Converting functions *****************************************************)
 
 let tref_uref u =
    let s = str_uref u in