From 691f90554fe985a5ef67a7e82fb684ab10024fac Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 4 Sep 2002 17:00:54 +0000 Subject: [PATCH] textual parser fixed --- .../cic_textual_parser/cicTextualLexer.mll | 2 +- .../cic_textual_parser/cicTextualParser.mly | 4 ++- .../cic_textual_parser/cicTextualParser0.ml | 4 +++ helm/ocaml/mathql/.depend | 6 ++-- helm/ocaml/mathql/Makefile | 5 +-- helm/ocaml/mathql/mQueryUtil.ml | 33 ++++--------------- 6 files changed, 21 insertions(+), 33 deletions(-) diff --git a/helm/ocaml/cic_textual_parser/cicTextualLexer.mll b/helm/ocaml/cic_textual_parser/cicTextualLexer.mll index 31878bfe6..1be084795 100644 --- 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 b85be0754..af67f1c14 100644 --- 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 0a8414734..fe4bf0623 100644 --- 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 0d8aa0719..c898ba8b0 100644 --- 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 f9c0eb9d8..8cd40ee82 100644 --- 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 0cf8ebe08..8943e5675 100644 --- 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 = "" ^ s ^ " " - -let sub s = " " ^ s ^ " " - -let sub2 s = "" ^ s ^ "" - -let sym s = s - -let sep s = s - -let str s = "'" ^ s ^ "'" - -let pat s = "\"" ^ s ^ "\"" - -let res s = "\"" ^ s ^ "\"" - -let nl () = "
" - -let par () = "

" - -(* 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 -- 2.39.2