Interface change: the get_as_string and set_term methods of the term-editors

[helm.git] / helm / gTopLevel / gTopLevel.ml

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