X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=789a65ba5c87330d11d00c027ea602f733fb9cac;hb=bea50d8a7fdf4063d8bf42d2983734190457e030;hp=083bbc7ebac6ccfc279d69cd00911210519ae7c6;hpb=c2ad6c9e76a929cca23276aa0e9dbbfdd1ca469b;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 083bbc7eb..789a65ba5 100644
--- 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