X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=189f17d3ce5288329e50b66b9d85042b4efccb5f;hb=96134b9ec1030ed15cea00d751dd4d744463f62c;hp=e3f49893171f5c9e1faaa01931ff9a76eef72a77;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e3f498931..189f17d3c 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -39,11 +39,16 @@ open Printf;;
 
 module MQI  = MQueryInterpreter
 module MQIC = MQIConn
+module MQGT = MQGTypes
+module MQGU = MQGUtil
 module MQG  = MQueryGenerator
 
 (* GLOBAL CONSTANTS *)
 
+let mqi_flags = [MQIC.Postgres ; MQIC.Stat ; MQIC.Warn ; MQIC.Log] (* default MathQL interpreter options *)
+(*
 let mqi_flags = [] (* default MathQL interpreter options *)
+*)
 let mqi_handle = MQIC.init mqi_flags prerr_string
 
 let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
@@ -556,6 +561,9 @@ let refresh_proof (output : TermViewer.proof_viewer) =
    match !ProofEngine.proof with
       None -> assert false
     | Some (uri,metasenv,bo,ty) ->
+       let bo_fixed = Eta_fixing.eta_fix metasenv bo in
+       let ty_fixed = Eta_fixing.eta_fix metasenv ty in
+       ProofEngine.proof := Some(uri,metasenv,bo_fixed,ty_fixed);
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
@@ -569,7 +577,7 @@ prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ;
 end ;
        (*CSC: Wrong: [] is just plainly wrong *)
        uri,
-        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo_fixed, ty_fixed, []))
   in
    ignore (output#load_proof uri currentproof)
  with
@@ -1650,7 +1658,8 @@ let open_ () =
        Some (uri, metasenv, bo, ty) ;
       ProofEngine.goal := None ;
       refresh_goals notebook ;
-      refresh_proof output
+      refresh_proof output ;
+      !save_set_sensitive true
    with
       InvokeTactics.RefreshSequentException e ->
        output_html outputhtml
@@ -1752,32 +1761,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 =
@@ -1800,30 +1813,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 (p, sort) ->
      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 =
@@ -1846,30 +1848,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 =
@@ -1891,15 +1885,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),
@@ -1918,9 +1915,11 @@ 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 None must' only in
+   let query =
+    MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
+   in
    let results = MQI.execute mqi_handle query in 
     show_query_results results
   with
@@ -2043,10 +2042,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
@@ -2075,10 +2074,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
@@ -2135,7 +2134,7 @@ let searchPattern () =
       | None -> ()
       | Some metano ->
          let uris' =
-           TacticChaser.searchPattern
+           TacticChaser.matchConclusion
 	    mqi_handle
             ~output_html:(output_html outputhtml) ~choose_must ()
             ~status:(proof, metano)
@@ -2261,7 +2260,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
@@ -2752,12 +2752,34 @@ class rendering_window output (notebook : notebook) =
  let settings_menu = factory0#add_submenu "Settings" in
  let factory3 = new GMenu.factory settings_menu ~accel_group in
  let _ =
-  factory3#add_item "Edit Aliases" ~key:GdkKeysyms._A
+  factory3#add_item "Edit Aliases..." ~key:GdkKeysyms._A
    ~callback:edit_aliases in
  let _ = factory3#add_separator () in
  let _ =
   factory3#add_item "MathML Widget Preferences..." ~key:GdkKeysyms._P
    ~callback:(function _ -> (settings_window ())#show ()) in
+ let _ = factory3#add_separator () in
+ let _ =
+  factory3#add_item "Reload Stylesheets"
+   ~callback:
+     (function _ ->
+       ApplyStylesheets.reload_stylesheets () ;
+       if !ProofEngine.proof <> None then
+        try
+         refresh_goals notebook ;
+         refresh_proof output
+        with
+           InvokeTactics.RefreshSequentException e ->
+            output_html (outputhtml ())
+             ("<h1 color=\"red\">An error occurred while refreshing the " ^
+               "sequent: " ^ Printexc.to_string e ^ "</h1>") ;
+           (*notebook#remove_all_pages ~skip_switch_page_event:false ;*)
+           notebook#set_empty_page
+         | InvokeTactics.RefreshProofException e ->
+            output_html (outputhtml ())
+             ("<h1 color=\"red\">An error occurred while refreshing the proof: "               ^ Printexc.to_string e ^ "</h1>") ;
+            output#unload
+     ) in
  (* accel group *)
  let _ = window#add_accel_group accel_group in
  (* end of menus *)