+let locate rendering_window () =
+ let inputt = (rendering_window#inputt : GEdit.text) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let inputlen = inputt#length in
+ let input = inputt#get_chars 0 inputlen in
+ try
+ output_html outputhtml (Mquery.locate input) ;
+ inputt#delete_text 0 inputlen
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
+;;
+
+let backward rendering_window () =
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let result =
+ match !ProofEngine.goal with
+ | None -> ""
+ | Some (_, (_, t)) -> (Mquery.backward t)
+ in
+ output_html outputhtml result
+