From: Claudio Sacerdoti Coen Date: Wed, 7 May 2003 11:47:43 +0000 (+0000) Subject: Interface change: the get_as_string and set_term methods of the term-editors X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=2afbca45037c56264d1889ced69b5f4844b9ecb9 Interface change: the get_as_string and set_term methods of the term-editors now work on an unquoted string: the string is TeX quoted (i.e. '$' are inserted at the beginning and end and '_' are quoted) by set_term and unquoted by get_as_string. This solves in an almost clean way the problem of hbugs (that had to quote the string). The solution is maybe still partial since it is not always possible to serialize/deserialize the input to a string. An improvement (???) would be to make the output type of get_as_string opaque and provide two set_term: the first one's input would be the opaque data type and the second one would be a CIC term. Changes #54. --- diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 4f6cab6af..3dd457384 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -1518,7 +1518,12 @@ let new_proof () = okb#misc#set_sensitive (b && uri_entry#text <> "")) in let _ = +let xxx = inputt#get_as_string in +prerr_endline ("######################## " ^ xxx) ; + newinputt#set_term xxx ; +(* newinputt#set_term inputt#get_as_string ; +*) inputt#reset in let _ = uri_entry#connect#changed diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml index 5392fae85..753f3fc78 100644 --- a/helm/gTopLevel/hbugs.ml +++ b/helm/gTopLevel/hbugs.ml @@ -124,13 +124,9 @@ module Initialize (Tactics: InvokeTactics.Tactics) : Unit = | Use_left_Luke -> Tactics.left () | Use_right_Luke -> Tactics.right () | Use_apply_Luke term -> - (* CSC: patch momentanea: la stringa deve essere nel formato *) - (* CSC: corretto (ovvero quotata se e' TeX ;-((( *) - let term = - let term' = String.sub term 4 (String.length term - 4) in - "$" ^ Str.global_replace (Str.regexp "_") "\\_" term' ^ "$" - in - Tactics.apply ~term () + (* we remove the "cic:" prefix *) + let term' = String.sub term 4 (String.length term - 4) in + Tactics.apply ~term:term' () | Hints _ -> assert false let _ = use_hint_callback := use_hint diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index 48f5adb63..310efd176 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -38,11 +38,13 @@ class type term_editor = object method coerce : GObj.widget + (* get_as_string returns the unquoted string *) method get_as_string : string method get_metasenv_and_term : context:Cic.context -> metasenv:Cic.metasenv -> Cic.metasenv * Cic.term method reset : unit + (* The input of set_term is unquoted *) method set_term : string -> unit method id_to_uris : Disambiguate.domain_and_interpretation ref end @@ -80,6 +82,7 @@ module Make(C:Disambiguate.Callbacks) = self#reset ; ignore ((input#insert_text txt) ~pos:0) (* CSC: this method should disappear *) + (* get_as_string returns the unquoted string *) method get_as_string = input#get_chars 0 input#length method get_metasenv_and_term ~context ~metasenv = diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index 55746ff1e..ce51bdbe8 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -26,6 +26,7 @@ class type term_editor = object method coerce : GObj.widget + (* get_as_string returns the unquoted string *) method get_as_string : string method get_metasenv_and_term : context:Cic.context -> diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index b8375b3ea..18c2215b5 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -38,11 +38,13 @@ class type term_editor = object method coerce : GObj.widget + (* get_as_string returns the unquoted string *) method get_as_string : string method get_metasenv_and_term : context:Cic.context -> metasenv:Cic.metasenv -> Cic.metasenv * Cic.term method reset : unit + (* The input of set_term is unquoted *) method set_term : string -> unit method id_to_uris : Disambiguate.domain_and_interpretation ref end @@ -165,18 +167,22 @@ module Make(C:Disambiguate.Callbacks) = ignore (Mathml_editor.thaw tex_editor) ; mmlwidget#thaw + (* The input of set_term is unquoted *) method set_term txt = mmlwidget#freeze ; ignore (Mathml_editor.freeze tex_editor) ; self#reset ; - (* we need to remove the initial and final '$' *) - let txt' = String.sub txt 1 (String.length txt - 2) in + let txt' = Str.global_replace (Str.regexp "_") "\\_" txt in String.iter (fun ch -> Mathml_editor.push tex_editor ch) txt' ; ignore (Mathml_editor.thaw tex_editor) ; mmlwidget#thaw + (* get_as_string returns the unquoted string *) method get_as_string = - Mathml_editor.get_tex tex_editor + let term = Mathml_editor.get_tex tex_editor in + Str.global_replace (Str.regexp "^\\$\\$?") "" + (Str.global_replace (Str.regexp "\\$\\$?$") "" + (Str.global_replace (Str.regexp "\\\\_") "_" term)) method get_metasenv_and_term ~context ~metasenv = let name_context = @@ -186,7 +192,7 @@ module Make(C:Disambiguate.Callbacks) = | None -> None ) context in - let lexbuf = Lexing.from_string self#get_as_string in + let lexbuf = Lexing.from_string (Mathml_editor.get_tex tex_editor) in let dom,mk_metasenv_and_expr = TexCicTextualParserContext.main ~context:name_context ~metasenv TexCicTextualLexer.token lexbuf diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli index 55746ff1e..beb21ec85 100644 --- a/helm/gTopLevel/texTermEditor.mli +++ b/helm/gTopLevel/texTermEditor.mli @@ -26,11 +26,13 @@ class type term_editor = object method coerce : GObj.widget + (* get_as_string returns the unquoted string *) method get_as_string : string method get_metasenv_and_term : context:Cic.context -> metasenv:Cic.metasenv -> Cic.metasenv * Cic.term method reset : unit + (* The input of set_term is unquoted *) method set_term : string -> unit method id_to_uris : Disambiguate.domain_and_interpretation ref end