X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=48c178918c019e9f6d3ad4ba1aac29d6ca8e9c7e;hb=1d2bd140d14561951f8214edf15abe4f40dcb649;hp=2b476a6745c278a7fe07953c747507344f630956;hpb=e34305aa0b9c8c9095e811b7ab720ffd4d283081;p=helm.git
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 2b476a674..48c178918 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -1085,44 +1085,71 @@ let check rendering_window scratch_window () =
("
" ^ Printexc.to_string e ^ "
") ;
;;
+exception NoObjectsLocated;;
+
+let user_uri_choice uris =
+ let uri =
+ match uris with
+ [] -> raise NoObjectsLocated
+ | [uri] -> uri
+ | uris ->
+ let choice =
+ GToolbox.question_box ~title:"Ambiguous result."
+ ~buttons:uris ~default:1
+ "Ambiguous result. Please, choose one."
+ in
+ List.nth uris (choice-1)
+ in
+ String.sub uri 4 (String.length uri - 4)
+;;
+
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
- output_html outputhtml (
- try
- match Str.split (Str.regexp "[ \t]+") input with
- | [] -> ""
- | head :: tail ->
- inputt#delete_text 0 inputlen;
- MQueryGenerator.locate_html head
- with
- e -> "" ^ Printexc.to_string e ^ "
"
- )
+ try
+ match Str.split (Str.regexp "[ \t]+") input with
+ [] -> ()
+ | head :: tail ->
+ inputt#delete_text 0 inputlen ;
+ let MathQL.MQRefs uris, html = MQueryGenerator.locate head in
+ output_html outputhtml html ;
+ let uri' = user_uri_choice uris in
+ ignore ((inputt#insert_text uri') ~pos:0)
+ with
+ e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
;;
let backward rendering_window () =
- let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) 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 (_, ey ,ty) =
- List.find (function (m,_,_) -> m=metano) metasenv
- in
- MQueryGenerator.backward metasenv ey ty level
- in
- output_html outputhtml result
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) 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
+ try
+ match !ProofEngine.goal with
+ None -> ()
+ | Some metano ->
+ let (_, ey ,ty) = List.find (function (m,_,_) -> m=metano) metasenv in
+ let MathQL.MQRefs uris, html =
+ MQueryGenerator.backward metasenv ey ty level
+ in
+ output_html outputhtml html ;
+ let uri' = user_uri_choice uris in
+ inputt#delete_text 0 inputlen ;
+ ignore ((inputt#insert_text uri') ~pos:0)
+ with
+ e ->
+ output_html outputhtml
+ ("" ^ Printexc.to_string e ^ "
")
;;
let choose_selection
@@ -1494,15 +1521,18 @@ end;;
(* MAIN *)
+let rendering_window = ref None;;
+
let initialize_everything () =
let module U = Unix in
let output = GMathView.math_view ~width:400 ~height:280 ()
and proofw = GMathView.math_view ~width:400 ~height:275 ()
and label = GMisc.label ~text:"gTopLevel" () in
- let rendering_window =
+ let rendering_window' =
new rendering_window output proofw label
in
- rendering_window#show () ;
+ rendering_window := Some rendering_window' ;
+ rendering_window'#show () ;
GMain.Main.main ()
;;
@@ -1513,12 +1543,22 @@ let _ =
MQueryGenerator.init () ;
CicTextualParser0.set_locate_object
(function id ->
- let MathQL.MQRefs uris = MQueryGenerator.locate id in
+ let MathQL.MQRefs uris, html = MQueryGenerator.locate id in
+ begin
+ match !rendering_window with
+ None -> assert false
+ | Some rw -> output_html rw#outputhtml html ;
+ end ;
let uri =
match uris with
[] ->
- (GToolbox.input_string ~title:"Unknown input"
- ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+ (match
+ (GToolbox.input_string ~title:"Unknown input"
+ ("No URI matching \"" ^ id ^ "\" found. Please enter its URI"))
+ with
+ None -> None
+ | Some uri -> Some ("cic:" ^ uri)
+ )
| [uri] -> Some uri
| _ ->
let choice =