*** empty log message ***

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 083bbc7ebac6ccfc279d69cd00911210519ae7c6..789a65ba5c87330d11d00c027ea602f733fb9cac 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -990,31 +990,38 @@ let locate rendering_window () =
  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>")
+  output_html outputhtml (
+     try
+        match Str.split (Str.regexp "[ \t]+") input with
+           | [] -> ""
+           | head :: tail ->
+              inputt#delete_text 0 inputlen;
+              Mquery.locate head 
+     with
+        e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
+  )
 ;;
 
 let backward rendering_window () =
    let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
-   let metasenv =
-    match !ProofEngine.proof with
-       None -> assert false
-     | Some (_,metasenv,_,_) -> metasenv
-   in
-   let result =
-      match !ProofEngine.goal with
-         | None -> ""
-         | Some metano ->
-            let (_,_,ty) =
-             List.find (function (m,_,_) -> m=metano) metasenv
-            in
-             Mquery.backward ty
-      in 
+   let inputt = (rendering_window#inputt : GEdit.text) in
+    let inputlen = inputt#length in
+    let input = inputt#get_chars 0 inputlen in
+    let level = int_of_string input in
+    let metasenv =
+     match !ProofEngine.proof with
+        None -> assert false
+      | Some (_,metasenv,_,_) -> metasenv
+    in
+    let result =
+       match !ProofEngine.goal with
+          | None -> ""
+          | Some metano ->
+             let (_,_,ty) =
+              List.find (function (m,_,_) -> m=metano) metasenv
+             in
+              Mquery.backward ty level
+       in 
    output_html outputhtml result
       
 let choose_selection