snapshot, notably:

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index e565c03a787e6f0c1cd6b4eaaef9afba9b1048cf..6a5e2e51debf5c20bedc785d079ffba14e357c60 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -61,13 +61,10 @@ let disambiguator =
     ~chooseUris:(interactive_user_uri_choice ~gui)
     ~chooseInterp:(interactive_interp_choice ~gui)
     ()
-let proof_viewer =
-  let frame = GBin.frame ~packing:(gui#proof#scrolledProof#add) ~show:true () in
-  MatitaMathView.proof_viewer ~show:true ~packing:(frame#add) ()
+let proof_viewer = MatitaMathView.proof_viewer_instance ()
 let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
 let sequents_viewer =
   let set_goal goal =
-    debug_print (sprintf "Setting goal %d" goal);
     if not (has_proof ()) then assert false;
     (get_proof ())#set_goal goal
   in
@@ -77,12 +74,8 @@ let sequents_viewer =
 let new_proof (proof: MatitaTypes.proof) =
   let xmldump_observer _ _ =  print_endline proof#toString in
   let proof_observer _ (status, ()) =
-    debug_print "proof_observer";
     let ((uri_opt, _, _, _), _) = status in
-    let uri = MatitaTypes.unopt_uri uri_opt in
-    debug_print "apply transformation";
     proof_viewer#load_proof status;
-    debug_print "/proof_observer"
   in
   let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
     sequents_viewer#reset;
@@ -96,8 +89,10 @@ let new_proof (proof: MatitaTypes.proof) =
     sequents_observer);
   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
     proof_observer);
+(*
   ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
     xmldump_observer);
+*)
   proof#notify;
   set_proof (Some proof)
 
@@ -135,6 +130,43 @@ let ask_term ?(title = "term input") ?(msg = "insert term") () =
       Some term
   | None -> None
 
+(** {2 Script window handling} *)
+
+let script_forward _ =
+  let buf = gui#script#scriptTextView#buffer in
+  let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+  interpreter#evalPhrase
+    (buf#get_text ~start:locked_iter ~stop:buf#end_iter ());
+  gui#lockScript (locked_iter#offset + interpreter#endOffset)
+
+let script_jump _ =
+  let buf = gui#script#scriptTextView#buffer in
+  let locked_iter = buf#get_iter_at_mark (`NAME "locked") in
+  let cursor_iter = buf#get_iter_at_mark (`NAME "insert") in
+  let raw_text = buf#get_text ~start:locked_iter ~stop:cursor_iter () in
+  let len = String.length raw_text in
+  let rec parse offset =
+    if offset < len then begin
+      interpreter#evalPhrase ~transparent:true
+        (String.sub raw_text offset (len - offset));
+      let new_offset = interpreter#endOffset + offset in
+      gui#lockScript (new_offset + locked_iter#offset);
+      parse new_offset
+    end
+  in
+  try
+    parse 0
+  with CicTextualParser2.Parse_error _ -> ()
+
+let script_back _ = not_implemented "script_back"
+
+let load_script fname =
+  gui#script#scriptTextView#buffer#set_text (input_file fname);
+  gui#script#scriptWin#show ();
+  gui#main#showScriptMenuItem#set_active true
+
+(** {2 GUI callbacks} *)
+
 let _ =
   gui#setQuitCallback quit;
   gui#setPhraseCallback interpreter#evalPhrase;
@@ -156,14 +188,14 @@ let _ =
   ignore (gui#main#openMenuItem#connect#activate (fun _ ->
     match gui#chooseFile () with
     | None -> ()
-    | Some f when is_proof_script f ->
-        gui#script#scriptTextView#buffer#set_text (input_file f);
-        gui#script#scriptWin#show ();
-        gui#main#showScriptMenuItem#set_active true
+    | Some f when is_proof_script f -> load_script f
     | Some f ->
         gui#console#echo_error (sprintf
           "Don't know what to do with file: %s\nUnrecognized file format."
           f)));
+  ignore (gui#script#scriptWinForwardButton#connect#clicked script_forward);
+  ignore (gui#script#scriptWinBackButton#connect#clicked script_back);
+  ignore (gui#script#scriptWinJumpButton#connect#clicked script_jump);
   let tac_w_term name tac _ =
     match ask_term ~title:name ~msg:("term for " ^ name) () with
     | Some term -> (get_proof ())#apply_tactic (tac ~term)
@@ -235,5 +267,9 @@ let _ =
 
   (** </DEBUGGING> *)
 
-let _ = GtkThread.main ()
+let _ =
+  (try
+    load_script Sys.argv.(1)
+  with Invalid_argument _ -> ());
+  GtkThread.main ()