From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 16:07:42 +0000 (+0000) Subject: (temporary, waiting for abstraction over disambiguators) ported to Andrea & X-Git-Tag: V_0_5_1_4~9 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c1cf3479d53bbe813c254433b6b9d4d5839065d2;p=helm.git (temporary, waiting for abstraction over disambiguators) ported to Andrea & Zack's disambiguator --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index fa1ad6ea8..d54236fd8 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2000-2003, HELM Team. +(* Copyright (C) 2000-2004, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -744,11 +744,16 @@ let edit_aliases () = ignore (cancelb#connect#clicked window#destroy) ; ignore (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - let dom,resolve_id = !id_to_uris in + let resolve_id = !id_to_uris in ignore (input#buffer#insert ~iter:(input#buffer#get_iter_at_char 0) - (String.concat "\n" - (List.map + (Disambiguate_types.Environment.fold + (fun i v s -> + match i with + | Disambiguate_types.Id id -> s ^ sprintf "alias %s %s\n" id (fst v) + | _ -> "") + resolve_id "")) ; +(* (function v -> let uri = match resolve_id v with @@ -764,11 +769,12 @@ let edit_aliases () = (* CSC: To be implemented *) assert false )^ " " ^ (string_of_cic_textual_parser_uri uri) - ) dom))) ; + ) +*) window#show () ; GtkThread.main (); if !chosen then - let dom,resolve_id = + let resolve_id = let inputtext = input#buffer#get_text () in let regexpr = let alfa = "[a-zA-Z_-]" in @@ -783,26 +789,21 @@ let edit_aliases () = let rec aux n = try let n' = Str.search_forward regexpr inputtext n in - let id = CicTextualParser0.Id (Str.matched_group 2 inputtext) in - let uri = - MQueryMisc.cic_textual_parser_uri_of_string - ("cic:" ^ (Str.matched_group 5 inputtext)) - in - let dom,resolve_id = aux (n' + 1) in - if List.mem id dom then - dom,resolve_id + 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 - id::dom, - (function id' -> - if id = id' then - Some (CicTextualParser0.Uri uri) - else resolve_id id') + let term = Disambiguate.term_of_uri uri in + (Disambiguate_types.Environment.add id (uri, (fun _ _ _ -> term)) + resolve_id) with Not_found -> TermEditor.empty_id_to_uris in aux 0 in - id_to_uris := (dom,resolve_id) + id_to_uris := resolve_id ;; let proveit () = @@ -901,7 +902,7 @@ let Cic2acic.acic_object_of_cic_object obj in let mml = - ApplyStylesheets.mml_of_cic_object + ChosenTransformer.mml_of_cic_object ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types in window#set_title (UriManager.string_of_uri uri) ; @@ -1082,12 +1083,12 @@ exception AmbiguousInput;; (* A WIDGET TO ENTER CIC TERMS *) +(* module ChosenTermEditor = TexTermEditor;; module ChosenTextualParser0 = TexCicTextualParser0;; -(* +*) module ChosenTermEditor = TermEditor;; module ChosenTextualParser0 = CicTextualParser0;; -*) module Callbacks = struct @@ -1520,7 +1521,6 @@ let new_proof () = in let _ = let xxx = inputt#get_as_string in -prerr_endline ("######################## " ^ xxx) ; newinputt#set_term xxx ; (* newinputt#set_term inputt#get_as_string ; @@ -2156,7 +2156,6 @@ let searchPattern () = let choose_selection mmlwidget (element : Gdome.element option) = let module G = Gdome in - prerr_endline "Il bandolo" ; let rec aux element = if element#hasAttributeNS ~namespaceURI:Misc.helmns @@ -2824,7 +2823,7 @@ class rendering_window output (notebook : notebook) = factory3#add_item "Reload Stylesheets" ~callback: (function _ -> - ApplyStylesheets.reload_stylesheets () ; + ChosenTransformer.reload_stylesheets () ; if ProofEngine.get_proof () <> None then try refresh_goals notebook ; diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index d4f040a9a..f034c45b1 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -33,6 +33,10 @@ (* *) (******************************************************************************) +open Printf + +open Disambiguate_types + (* A WIDGET TO ENTER CIC TERMS *) class type term_editor = @@ -46,19 +50,18 @@ class type term_editor = method reset : unit (* The input of set_term is unquoted *) method set_term : string -> unit - method id_to_uris : Disambiguate.domain_and_interpretation ref + method id_to_uris : environment ref end -;; -let empty_id_to_uris = ([],function _ -> None);; +let empty_id_to_uris = Environment.empty -module Make(C:Disambiguate.Callbacks) = +module Make(C: Callbacks) = struct module Disambiguate' = Disambiguate.Make(C);; - class term_editor_impl mqi_handle ?packing ?width ?height ?isnotempty_callback - ?share_id_to_uris_with () : term_editor + class term_editor_impl mqi_handle ?packing ?width ?height + ?isnotempty_callback ?share_id_to_uris_with () : term_editor = let id_to_uris = match share_id_to_uris_with with @@ -74,17 +77,21 @@ module Make(C:Disambiguate.Callbacks) = (function () -> callback (input#buffer#char_count > 0))) in object(self) + method coerce = input#coerce + method reset = input#buffer#delete input#buffer#start_iter input#buffer#end_iter (* CSC: txt is now a string, but should be of type Cic.term *) + method set_term txt = self#reset ; ignore (input#buffer#insert txt) + (* CSC: this method should disappear *) (* get_as_string returns the unquoted string *) - method get_as_string = - input#buffer#get_text () + method get_as_string = input#buffer#get_text () + method get_metasenv_and_term ~context ~metasenv = let name_context = List.map @@ -93,21 +100,20 @@ module Make(C:Disambiguate.Callbacks) = | None -> None ) context in - let lexbuf = Lexing.from_string (input#buffer#get_text ()) in - let dom,mk_metasenv_and_expr = - CicTextualParserContext.main - ~context:name_context ~metasenv CicTextualLexer.token lexbuf - in - let id_to_uris',metasenv,expr = - Disambiguate'.disambiguate_input mqi_handle - context metasenv dom mk_metasenv_and_expr ~id_to_uris:!id_to_uris - in - id_to_uris := id_to_uris' ; - metasenv,expr + let term = + Parser.parse_term (Stream.of_string (input#buffer#get_text ())) + in + let id_to_uris',metasenv,expr = + Disambiguate'.disambiguate_term mqi_handle context metasenv term + ~aliases:!id_to_uris + in + id_to_uris := id_to_uris'; + (metasenv, expr) + method id_to_uris = id_to_uris end let term_editor = new term_editor_impl end -;; + diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index ce51bdbe8..77fd2285d 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -23,6 +23,8 @@ * http://cs.unibo.it/helm/. *) +open Disambiguate_types + class type term_editor = object method coerce : GObj.widget @@ -33,12 +35,12 @@ class type term_editor = metasenv:Cic.metasenv -> Cic.metasenv * Cic.term method reset : unit method set_term : string -> unit - method id_to_uris : Disambiguate.domain_and_interpretation ref + method id_to_uris : environment ref end -val empty_id_to_uris : Disambiguate.domain_and_interpretation +val empty_id_to_uris : environment -module Make (C : Disambiguate.Callbacks) : +module Make (C : Callbacks) : sig val term_editor : MQIConn.handle ->