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.
okb#misc#set_sensitive (b && uri_entry#text <> ""))
in
let _ =
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 ;
newinputt#set_term inputt#get_as_string ;
inputt#reset in
let _ =
uri_entry#connect#changed
inputt#reset in
let _ =
uri_entry#connect#changed
| Use_left_Luke -> Tactics.left ()
| Use_right_Luke -> Tactics.right ()
| Use_apply_Luke term ->
| 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
| Hints _ -> assert false
let _ = use_hint_callback := use_hint
class type term_editor =
object
method coerce : GObj.widget
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
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
method set_term : string -> unit
method id_to_uris : Disambiguate.domain_and_interpretation ref
end
self#reset ;
ignore ((input#insert_text txt) ~pos:0)
(* CSC: this method should disappear *)
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 =
method get_as_string =
input#get_chars 0 input#length
method get_metasenv_and_term ~context ~metasenv =
class type term_editor =
object
method coerce : GObj.widget
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 ->
method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
class type term_editor =
object
method coerce : GObj.widget
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
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
method set_term : string -> unit
method id_to_uris : Disambiguate.domain_and_interpretation ref
end
ignore (Mathml_editor.thaw tex_editor) ;
mmlwidget#thaw
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 ;
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
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 *)
- 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 =
method get_metasenv_and_term ~context ~metasenv =
let name_context =
| None -> None
) context
in
| 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
let dom,mk_metasenv_and_expr =
TexCicTextualParserContext.main
~context:name_context ~metasenv TexCicTextualLexer.token lexbuf
class type term_editor =
object
method coerce : GObj.widget
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
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
method set_term : string -> unit
method id_to_uris : Disambiguate.domain_and_interpretation ref
end