]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/gTopLevel.ml
Reindentation.
[helm.git] / helm / gTopLevel / gTopLevel.ml
index 0f2f73c281740a39ef386991b15c560051421bb8..7d3985af3a56b63ef24059f16bac82e8f3a06232 100644 (file)
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000-2002, HELM Team.
+(* Copyright (C) 2000-2003, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -39,6 +39,8 @@ open Printf;;
 
 module MQI  = MQueryInterpreter
 module MQIC = MQIConn
+module MQGT = MQGTypes
+module MQGU = MQGUtil
 module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
@@ -75,6 +77,16 @@ let prooffiletype =
   Not_found -> "/public/currentprooftype"
 ;;
 
+let environmentfile =
+ try
+  Sys.getenv "GTOPLEVEL_ENVIRONMENTFILE"
+ with
+  Not_found -> "/public/environment"
+;;
+
+let restore_environment_on_boot = true ;;
+let notify_hbugs_on_goal_change = false ;;
+
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
 let htmlheader_and_content = ref htmlheader;;
@@ -215,7 +227,8 @@ let check_window outputhtml uris =
  in
   ignore
    (notebook#connect#switch_page
-     (function i -> Lazy.force (List.nth render_terms i)))
+     (function i ->
+       Lazy.force (List.nth render_terms i)))
 ;;
 
 exception NoChoice;;
@@ -467,7 +480,7 @@ let save_obj uri obj =
 ;;
 
 let qed () =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,[],bo,ty) ->
      if
@@ -556,20 +569,17 @@ let mk_fresh_name_callback context name ~typ =
 let refresh_proof (output : TermViewer.proof_viewer) =
  try
   let uri,currentproof =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> assert false
     | Some (uri,metasenv,bo,ty) ->
+       ProofEngine.set_proof (Some (uri,metasenv,bo,ty)) ;
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.clear ()" ;
          Hbugs.clear ()
         end
        else
-begin
-prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
         Hbugs.notify () ;
-end ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,
         (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
@@ -577,12 +587,16 @@ end ;
    ignore (output#load_proof uri currentproof)
  with
   e ->
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,metasenv,bo,ty) ->
 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
    raise (InvokeTactics.RefreshProofException e)
 
+let set_proof_engine_goal g =
+ ProofEngine.goal := g
+;;
+
 let refresh_goals ?(empty_notebook=true) notebook =
  try
   match !ProofEngine.goal with
@@ -596,7 +610,7 @@ let refresh_goals ?(empty_notebook=true) notebook =
        notebook#proofw#unload
    | Some metano ->
       let metasenv =
-       match !ProofEngine.proof with
+       match ProofEngine.get_proof () with
           None -> assert false
         | Some (_,metasenv,_,_) -> metasenv
       in
@@ -612,18 +626,18 @@ let refresh_goals ?(empty_notebook=true) notebook =
           notebook#remove_all_pages ~skip_switch_page_event ;
           List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
         in
-          if empty_notebook then
-           begin
-            regenerate_notebook () ;
-            notebook#set_current_page
-             ~may_skip_switch_page_event:false metano
-           end
-          else
-           begin
-            notebook#set_current_page
-             ~may_skip_switch_page_event:true metano ;
-            notebook#proofw#load_sequent metasenv currentsequent
-           end
+         if empty_notebook then
+          begin
+           regenerate_notebook () ;
+           notebook#set_current_page
+            ~may_skip_switch_page_event:false metano
+          end
+         else
+          begin
+           notebook#set_current_page
+            ~may_skip_switch_page_event:true metano ;
+           notebook#proofw#load_sequent metasenv currentsequent
+          end
  with
   e ->
 let metano =
@@ -632,7 +646,7 @@ let metano =
    | Some m -> m
 in
 let metasenv =
- match !ProofEngine.proof with
+ match ProofEngine.get_proof () with
     None -> assert false
   | Some (_,metasenv,_,_) -> metasenv
 in
@@ -662,8 +676,18 @@ module InvokeTacticsCallbacks =
  end
 ;;
 module InvokeTactics' = InvokeTactics.Make (InvokeTacticsCallbacks);;
+
 (* Just to initialize the Hbugs module *)
 module Ignore = Hbugs.Initialize (InvokeTactics');;
+Hbugs.set_describe_hint_callback (fun hint ->
+  match hint with
+  | Hbugs_types.Use_apply_Luke term ->
+      let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
+      check_window outputhtml [term]
+  | _ -> ())
+;;
+
+let dummy_uri = "/dummy.con"
 
   (** load an unfinished proof from filesystem *)
 let load_unfinished_proof () =
@@ -672,7 +696,7 @@ let load_unfinished_proof () =
  let notebook = (rendering_window ())#notebook in
   try
    match 
-    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:"/dummy.con"
+    GToolbox.input_string ~title:"Load Unfinished Proof" ~text:dummy_uri
      "Choose an URI:"
    with
       None -> raise NoChoice
@@ -681,14 +705,13 @@ let load_unfinished_proof () =
         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
-            ProofEngine.proof :=
-             Some (uri, metasenv, bo, ty) ;
-            ProofEngine.goal :=
+            ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+            refresh_proof output ;
+            set_proof_engine_goal
              (match metasenv with
                  [] -> None
                | (metano,_,_)::_ -> Some metano
              ) ;
-            refresh_proof output ;
             refresh_goals notebook ;
              output_html outputhtml
               ("<h1 color=\"Green\">Current proof type loaded from " ^
@@ -856,7 +879,7 @@ let setgoal metano =
  let notebook = (rendering_window ())#notebook in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let metasenv =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> assert false
     | Some (_,metasenv,_,_) -> metasenv
   in
@@ -1479,6 +1502,8 @@ let new_proof () =
  let uri_entry =
   GEdit.entry ~editable:true
    ~packing:(hbox#pack ~expand:true ~fill:true ~padding:5) () in
+ uri_entry#set_text dummy_uri;
+ uri_entry#select_region ~start:1 ~stop:(String.length dummy_uri);
  let hbox1 =
   GPack.hbox ~border_width:0
    ~packing:(vbox#pack ~expand:false ~fill:false ~padding:5) () in
@@ -1557,9 +1582,9 @@ prerr_endline ("######################## " ^ xxx) ;
   try
    let metasenv,expr = !get_metasenv_and_term () in
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
-     ProofEngine.proof :=
-      Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr) ;
-     ProofEngine.goal := Some 1 ;
+     ProofEngine.set_proof
+      (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+     set_proof_engine_goal (Some 1) ;
      refresh_goals notebook ;
      refresh_proof output ;
      !save_set_sensitive true ;
@@ -1600,7 +1625,7 @@ let check scratch_window () =
  let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   let metasenv =
-   match !ProofEngine.proof with
+   match ProofEngine.get_proof () with
       None -> []
     | Some (_,metasenv,_,_) -> metasenv
   in
@@ -1649,9 +1674,8 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.proof :=
-       Some (uri, metasenv, bo, ty) ;
-      ProofEngine.goal := None ;
+      ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+      set_proof_engine_goal None ;
       refresh_goals notebook ;
       refresh_proof output ;
       !save_set_sensitive true
@@ -1756,32 +1780,36 @@ let refine_constraints (must_obj,must_rel,must_sort) =
   GBin.scrolled_window ~border_width:10 ~height ~width:600
    ~packing:(vbox'#pack ~expand:true ~fill:true ~padding:5) () in
  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
+ let mk_depth_button (hbox:GPack.box) d =
+    let mutable_ref = ref (Some d) in
+    let depthb =
+     GButton.toggle_button
+      ~label:("depth = " ^ string_of_int d) 
+      ~active:true
+      ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
+    in
+     ignore
+      (depthb#connect#toggled
+       (function () ->
+        let sel_depth = if depthb#active then Some d else None in
+         mutable_ref := sel_depth
+       )) ; mutable_ref
+ in
  let rel_constraints =
   List.map
-   (function (position,depth) ->
+   (function p ->
      let hbox =
       GPack.hbox
        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
      let lMessage =
       GMisc.label
-       ~text:position
+       ~text:(MQGU.text_of_position (p:>MQGT.full_position))
        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
-     match depth with
-        None -> position, ref None
-      | Some depth' ->
-         let mutable_ref = ref (Some depth') in
-         let depthb =
-          GButton.toggle_button
-           ~label:("depth = " ^ string_of_int depth') ~active:true
-           ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
-         in
-          ignore
-           (depthb#connect#toggled
-             (function () ->
-               let sel_depth = if depthb#active then Some depth' else None in
-                mutable_ref := sel_depth
-            )) ;
-          position, mutable_ref
+     match p with
+      | `MainHypothesis None 
+      | `MainConclusion None -> p, ref None
+      | `MainHypothesis (Some depth') 
+      | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth'
    ) must_rel in
  (* Sort constraints *)
  let label =
@@ -1804,30 +1832,19 @@ let refine_constraints (must_obj,must_rel,must_sort) =
  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
  let sort_constraints =
   List.map
-   (function (position,depth,sort) ->
+   (function (psort) ->
      let hbox =
       GPack.hbox
        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
      let lMessage =
       GMisc.label
-       ~text:(sort ^ " " ^ position)
+       ~text:(MQGU.text_of_sort sort ^ " " ^ MQGU.text_of_position (p:>MQGT.full_position))
        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
-     match depth with
-        None -> position, ref None, sort
-      | Some depth' ->
-         let mutable_ref = ref (Some depth') in
-         let depthb =
-          GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
-           ~active:true
-           ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
-         in
-          ignore
-           (depthb#connect#toggled
-             (function () ->
-               let sel_depth = if depthb#active then Some depth' else None in
-                mutable_ref := sel_depth
-            )) ;
-          position, mutable_ref, sort
+     match p with
+      | `MainHypothesis None 
+      | `MainConclusion None -> p, ref None, sort
+      | `MainHypothesis (Some depth') 
+      | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', sort
    ) must_sort in
  (* Obj constraints *)
  let label =
@@ -1850,30 +1867,22 @@ let refine_constraints (must_obj,must_rel,must_sort) =
  let scrolled_vbox = GPack.vbox ~packing:scrolled_window#add_with_viewport () in
  let obj_constraints =
   List.map
-   (function (uri,position,depth) ->
+   (function (p, uri) ->
      let hbox =
       GPack.hbox
        ~packing:(scrolled_vbox#pack ~expand:false ~fill:false ~padding:5) () in
      let lMessage =
       GMisc.label
-       ~text:(uri ^ " " ^ position)
+       ~text:(uri ^ " " ^ (MQGU.text_of_position p))
        ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
-     match depth with
-        None -> uri, position, ref None
-      | Some depth' ->
-         let mutable_ref = ref (Some depth') in
-         let depthb =
-          GButton.toggle_button ~label:("depth = " ^ string_of_int depth')
-           ~active:true
-           ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) ()
-         in
-          ignore
-           (depthb#connect#toggled
-             (function () ->
-               let sel_depth = if depthb#active then Some depth' else None in
-                mutable_ref := sel_depth
-            )) ;
-          uri, position, mutable_ref
+     match p with
+      | `InBody
+      | `InHypothesis 
+      | `InConclusion 
+      | `MainHypothesis None 
+      | `MainConclusion None -> p, ref None, uri
+      | `MainHypothesis (Some depth') 
+      | `MainConclusion (Some depth') -> p, mk_depth_button hbox depth', uri
    ) must_obj in
  (* Confirm/abort buttons *)
  let hbox =
@@ -1895,15 +1904,18 @@ let refine_constraints (must_obj,must_rel,must_sort) =
   if !chosen then
    let chosen_must_rel =
     List.map
-     (function (position,ref_depth) -> position,!ref_depth) rel_constraints in
+     (function (position, ref_depth) -> MQGU.set_main_position position !ref_depth)
+     rel_constraints
+   in
    let chosen_must_sort =
     List.map
-     (function (position,ref_depth,sort) -> position,!ref_depth,sort)
+     (function (position, ref_depth, sort) -> 
+      MQGU.set_main_position position !ref_depth,sort)
      sort_constraints
    in
    let chosen_must_obj =
     List.map
-     (function (uri,position,ref_depth) -> uri,position,!ref_depth)
+     (function (position, ref_depth, uri) -> MQGU.set_full_position position !ref_depth, uri)
      obj_constraints
    in
     (chosen_must_obj,chosen_must_rel,chosen_must_sort),
@@ -1922,17 +1934,10 @@ let completeSearchPattern () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
-   let must = MQueryLevels2.get_constraints expr in
+   let must = CGSearchPattern.get_constraints expr in
    let must',only = refine_constraints must in
    let query =
-    MQG.query_of_constraints
-     (Some
-       ["http://www.cs.unibo.it/helm/schemas/schema-helm#MainConclusion" ;
-        "http://www.cs.unibo.it/helm/schemas/schema-helm#MainHypothesis" ;
-        "http://www.cs.unibo.it/helm/schemas/schema-helm#InConclusion" ;
-        "http://www.cs.unibo.it/helm/schemas/schema-helm#InHypothesis"
-       ])
-     must' only
+    MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
    in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
@@ -2056,10 +2061,10 @@ let choose_must list_of_must only =
      in
       ignore
        (List.map
-         (function (uri,position) ->
+         (function (position, uri) ->
            let n =
             clist#append 
-             [uri; if position then "MainConclusion" else "Conclusion"]
+             [uri; MQGUtil.text_of_position position]
            in
             clist#set_row ~selectable:false n
          ) must
@@ -2088,10 +2093,10 @@ let choose_must list_of_must only =
   in
    ignore
     (List.map
-      (function (uri,position) ->
+      (function (position, uri) ->
         let n =
          clist#append 
-          [uri; if position then "MainConclusion" else "Conclusion"]
+          [uri; MQGUtil.text_of_position position]
         in
          clist#set_row ~selectable:true n
       ) only
@@ -2140,7 +2145,7 @@ let searchPattern () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
     let proof =
-     match !ProofEngine.proof with
+     match ProofEngine.get_proof () with
         None -> assert false
       | Some proof -> proof
     in
@@ -2148,7 +2153,7 @@ let searchPattern () =
       | None -> ()
       | Some metano ->
          let uris' =
-           TacticChaser.searchPattern
+           TacticChaser.matchConclusion
            mqi_handle
             ~output_html:(output_html outputhtml) ~choose_must ()
             ~status:(proof, metano)
@@ -2274,7 +2279,8 @@ class settings_window output sw
    ~packing:(table#attach ~left:0 ~top:0 ~expand:`NONE) () in
  let font_size_spinb =
   let sadj =
-   GData.adjustment ~value:14.0 ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
+   GData.adjustment ~value:(float_of_int output#get_font_size)
+    ~lower:5.0 ~upper:50.0 ~step_incr:1.0 ()
   in
    GEdit.spin_button 
     ~adjustment:sadj ~packing:(table#attach ~left:1 ~top:0 ~fill:`NONE) () in
@@ -2648,14 +2654,47 @@ object(self)
        if not skip then
         try
          let (metano,setgoal,page) = List.nth !pages i in
-          ProofEngine.goal := Some metano ;
+          set_proof_engine_goal (Some metano) ;
           Lazy.force (page#compute) ;
-          Lazy.force setgoal
+          Lazy.force setgoal;
+          if notify_hbugs_on_goal_change then
+            Hbugs.notify ()
         with _ -> ()
     ))
 end
 ;;
 
+let dump_environment () =
+  try
+    let oc = open_out environmentfile in
+    output_html (outputhtml ()) "<b>Dumping environment ... </b><br />";
+    CicEnvironment.dump_to_channel
+      ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+      oc;
+    output_html (outputhtml ()) "<b>... done!</b><br />";
+    close_out oc
+  with exc ->
+    output_html (outputhtml ())
+      (Printf.sprintf
+        "<h1 color=\"red\">Dump failure, uncaught exception:%s</h1>"
+        (Printexc.to_string exc))
+;;
+let restore_environment () =
+  try
+    let ic = open_in environmentfile in
+    output_html (outputhtml ()) "<b>Restoring environment ... </b><br />";
+    CicEnvironment.restore_from_channel
+      ~callback:(fun uri -> output_html (outputhtml ()) (uri ^ "<br />"))
+      ic;
+    output_html (outputhtml ()) "<b>... done!</b><br />";
+    close_in ic
+  with exc ->
+    output_html (outputhtml ())
+      (Printf.sprintf
+        "<h1 color=\"red\">Restore failure, uncaught exception:%s</h1>"
+        (Printexc.to_string exc))
+;;
+
 (* Main window *)
 
 class rendering_window output (notebook : notebook) =
@@ -2698,6 +2737,11 @@ class rendering_window output (notebook : notebook) =
     factory1#add_item "Save Unfinished Proof" ~key:GdkKeysyms._S
       ~callback:save_unfinished_proof
    in
+   ignore (factory1#add_separator ()) ;
+   ignore (factory1#add_item "Clear Environment" ~callback:CicEnvironment.empty);
+   ignore (factory1#add_item "Dump Environment" ~callback:dump_environment);
+   ignore
+    (factory1#add_item "Restore Environment" ~callback:restore_environment);
    ignore
     (save_set_sensitive := function b -> save_menu_item#misc#set_sensitive b);
    ignore (!save_set_sensitive false);
@@ -2757,10 +2801,21 @@ class rendering_window output (notebook : notebook) =
  (* hbugs menu *)
  let hbugs_menu = factory0#add_submenu "HBugs" in
  let factory6 = new GMenu.factory hbugs_menu ~accel_group in
- let toggle_hbugs_menu_item =
+ let _ =
   factory6#add_check_item
     ~active:false ~key:GdkKeysyms._F5 ~callback:Hbugs.toggle "HBugs enabled"
  in
+ let _ =
+  factory6#add_item ~key:GdkKeysyms._Return ~callback:Hbugs.notify
+   "(Re)Submit status!"
+ in
+ let _ = factory6#add_separator () in
+ let _ =
+  factory6#add_item ~callback:Hbugs.start_web_services "Start Web Services"
+ in
+ let _ =
+  factory6#add_item ~callback:Hbugs.stop_web_services "Stop Web Services"
+ in
  (* settings menu *)
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in
@@ -2777,7 +2832,7 @@ class rendering_window output (notebook : notebook) =
    ~callback:
      (function _ ->
        ApplyStylesheets.reload_stylesheets () ;
-       if !ProofEngine.proof <> None then
+       if ProofEngine.get_proof () <> None then
         try
          refresh_goals notebook ;
          refresh_proof output
@@ -2877,7 +2932,8 @@ let initialize_everything () =
      Gdome_xslt.setDebugCallback
       (Some (print_error_as_html "XSLT Debug Message: "));
      rendering_window'#show () ;
-(*      Hbugs.toggle true; *)
+     if restore_environment_on_boot && Sys.file_exists environmentfile then
+       restore_environment ();
      GtkThread.main ()
 ;;