From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 18 Dec 2002 17:33:10 +0000 (+0000)
Subject: "Insert Query (Experts only)" menu item added.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=331dc1783c8572be9d5c7c0ba11fa2995539bbf6;p=helm.git

"Insert Query (Experts only)" menu item added.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e54f3a0df..eac6fad1b 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -2642,6 +2642,74 @@ let completeSearchPattern () =
      ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
 ;;
 
+let insertQuery () =
+ let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+  try
+   let chosen = ref None in
+   let window =
+    GWindow.window
+     ~modal:true ~title:"Insert Query (Experts Only)" ~border_width:2 () in
+   let vbox = GPack.vbox ~packing:window#add () in
+   let label =
+    GMisc.label ~text:"Insert Query. For Experts Only."
+     ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let scrolled_window =
+    GBin.scrolled_window ~border_width:10 ~height:400 ~width:600
+     ~packing:(vbox#pack ~expand:true ~fill:true ~padding:5) () in
+   let input = GEdit.text ~editable:true
+    ~packing:scrolled_window#add () in
+   let hbox =
+    GPack.hbox ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let okb =
+    GButton.button ~label:"Ok"
+     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let loadb =
+    GButton.button ~label:"Load from file..."
+     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+   let cancelb =
+    GButton.button ~label:"Abort"
+     ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+   ignore (window#connect#destroy GMain.Main.quit) ;
+   ignore (cancelb#connect#clicked window#destroy) ;
+   ignore
+    (okb#connect#clicked
+      (function () ->
+        chosen := Some (input#get_chars 0 input#length) ; window#destroy ())) ;
+   ignore
+    (loadb#connect#clicked
+      (function () ->
+        match
+         GToolbox.select_file ~title:"Select Query File" ()
+        with
+           None -> ()
+         | Some filename ->
+            let inch = open_in filename in
+             let rec read_file () =
+              try
+               let line = input_line inch in
+                line ^ "\n" ^ read_file ()
+              with
+               End_of_file -> ""
+             in
+              let text = read_file () in
+               input#delete_text 0 input#length ;
+               ignore (input#insert_text text ~pos:0))) ;
+   window#set_position `CENTER ;
+   window#show () ;
+   GMain.Main.main () ;
+   match !chosen with
+      None -> ()
+    | Some q ->
+       let results =
+        Mqint.execute (MQueryUtil.query_of_text (Lexing.from_string q))
+       in
+        show_query_results results
+  with
+   e ->
+    output_html outputhtml
+     ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+;;
+
 let choose_must list_of_must only =
  let chosen = ref None in
  let user_constraints = ref [] in
@@ -3378,6 +3446,9 @@ class rendering_window output (notebook : notebook) =
  let show_menu_item =
   factory4#add_item "Show..." ~key:GdkKeysyms._H ~callback:show
  in
+ let insert_query_item =
+  factory4#add_item "Insert Query (Experts Only)..." ~key:GdkKeysyms._U
+   ~callback:insertQuery in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in