("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
;;
+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 -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
- )
+ 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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
;;
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
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>")
;;
let choose_selection
(* 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 ()
;;
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 =