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
| 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
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
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 =
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 ->
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
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 =
| 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
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