From 6f7dbdfa37be6a1135df8169557eab5c92c485e2 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 23 Jan 2004 16:39:35 +0000 Subject: [PATCH] moved environmentP3 in cic_textual_parser2 and reshaped interface --- helm/gTopLevel/chosenTermEditor.mli | 2 +- helm/gTopLevel/disambiguatingParser.ml | 45 +------------------------ helm/gTopLevel/disambiguatingParser.mli | 8 ++--- helm/gTopLevel/gTopLevel.ml | 4 +-- helm/gTopLevel/termEditor.ml | 6 ++-- helm/gTopLevel/termEditor.mli | 2 +- 6 files changed, 13 insertions(+), 54 deletions(-) diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli index 962aa0532..ebd9a95e6 100644 --- a/helm/gTopLevel/chosenTermEditor.mli +++ b/helm/gTopLevel/chosenTermEditor.mli @@ -5,7 +5,7 @@ class type term_editor = method get_metasenv_and_term : context:Cic.context -> metasenv:Cic.metasenv -> Cic.metasenv * Cic.term - method environment : DisambiguatingParser.Environment.t ref + method environment : DisambiguatingParser.EnvironmentP3.t ref method reset : unit method set_term : string -> unit end diff --git a/helm/gTopLevel/disambiguatingParser.ml b/helm/gTopLevel/disambiguatingParser.ml index 057cacb42..8ce12c045 100644 --- a/helm/gTopLevel/disambiguatingParser.ml +++ b/helm/gTopLevel/disambiguatingParser.ml @@ -25,50 +25,7 @@ exception NoWellTypedInterpretation -module Environment = - struct - type t = Disambiguate_types.environment - - let empty = Disambiguate_types.Environment.empty - - let to_string env = -prerr_endline "TODO: implement and move away" ; - Disambiguate_types.Environment.fold - (fun i v s -> - match i with - | Disambiguate_types.Id id ->s ^ Printf.sprintf "alias %s %s\n" id (fst v) - | _ -> "") - env "" - - let of_string inputtext = - let regexpr = - let alfa = "[a-zA-Z_-]" in - let digit = "[0-9]" in - let ident = alfa ^ "\(" ^ alfa ^ "\|" ^ digit ^ "\)*" in - let blanks = "\( \|\t\|\n\)+" in - let nonblanks = "[^ \t\n]+" in - let uri = "/\(" ^ ident ^ "/\)*" ^ nonblanks in (* not very strict check *) - Str.regexp - ("alias" ^ blanks ^ "\(" ^ ident ^ "\)" ^ blanks ^ "\(" ^ uri ^ "\)") - in - let rec aux n = - try - let n' = Str.search_forward regexpr inputtext n in - let id = Disambiguate_types.Id (Str.matched_group 2 inputtext) in - let uri = "cic:" ^ (Str.matched_group 5 inputtext) in - let resolve_id = aux (n' + 1) in - if Disambiguate_types.Environment.mem id resolve_id then - resolve_id - else - let term = Disambiguate.term_of_uri uri in - (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term)) - resolve_id) - with - Not_found -> Disambiguate_types.Environment.empty - in - aux 0 - end -;; +module EnvironmentP3 = Disambiguate_types.EnvironmentP3 module Make (C : Disambiguate_types.Callbacks) = struct diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index 6edb84239..397799548 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -25,10 +25,10 @@ exception NoWellTypedInterpretation -module Environment : +module EnvironmentP3 : sig type t - val empty : t + val empty : string val to_string : t -> string val of_string : string -> t end @@ -40,8 +40,8 @@ module Make (C : Disambiguate_types.Callbacks) : Cic.context -> Cic.metasenv -> string -> - Environment.t -> (* previous interpretation status *) - Environment.t * (* new interpretation status *) + EnvironmentP3.t -> (* previous interpretation status *) + EnvironmentP3.t * (* new interpretation status *) Cic.metasenv * (* new metasenv *) Cic.term (* disambiguated term *) end diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 76ebe6cc6..8932d21a8 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -746,12 +746,12 @@ let edit_aliases () = (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; ignore (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) - (DisambiguatingParser.Environment.to_string !id_to_uris)) ; + (DisambiguatingParser.EnvironmentP3.to_string !id_to_uris)) ; window#show () ; GtkThread.main (); if !chosen then id_to_uris := - DisambiguatingParser.Environment.of_string (input#buffer#get_text ()) + DisambiguatingParser.EnvironmentP3.of_string (input#buffer#get_text ()) ;; let proveit () = diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index ca5cca601..668bf1502 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -48,7 +48,7 @@ class type term_editor = method reset : unit (* The input of set_term is unquoted *) method set_term : string -> unit - method environment : DisambiguatingParser.Environment.t ref + method environment : DisambiguatingParser.EnvironmentP3.t ref end module Make(C:Disambiguate_types.Callbacks) = @@ -61,7 +61,9 @@ module Make(C:Disambiguate_types.Callbacks) = = let environment = match share_environment_with with - None -> ref DisambiguatingParser.Environment.empty + None -> ref + (DisambiguatingParser.EnvironmentP3.of_string + DisambiguatingParser.EnvironmentP3.empty) | Some obj -> obj#environment in let input = GText.view ~editable:true ?width ?height ?packing () in diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index e9e725ed2..67b076505 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -33,7 +33,7 @@ class type term_editor = metasenv:Cic.metasenv -> Cic.metasenv * Cic.term method reset : unit method set_term : string -> unit - method environment : DisambiguatingParser.Environment.t ref + method environment : DisambiguatingParser.EnvironmentP3.t ref end module Make (C : Disambiguate_types.Callbacks) : -- 2.39.2