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 4f6cab6afd292fc3d10752bbcc1d8a25f5b5a851..3dd4573844b426b79ab0467c1c68d00eaa6d75cb 100644 (file)
--- 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 5392fae858729a9b3f6ce711728f927c16c7b054..753f3fc787e89d8cdc3690de376700ef16fb8c68 100644 (file)
--- 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 48f5adb63648b2ff04e92ddfee490fe45bb75f06..310efd176b0623693e855339fdffa619d53044e8 100644 (file)
--- 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 55746ff1e2641adcbf55af5e42a91d07dc19605f..ce51bdbe84fcba241fe8e67cc2006393e1b9c034 100644 (file)
--- 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 b8375b3eab0a9a861d8841c35a8cef17f4c714ed..18c2215b5f1be654f7ddf0cc36b734be2a3375ac 100644 (file)
--- 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 55746ff1e2641adcbf55af5e42a91d07dc19605f..beb21ec85003fb80bebe74f28ed11f221be3b01c 100644 (file)
--- 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