From de4483296d06aac3df4da10d5401b1f97c4350ab Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 16 May 2005 15:23:07 +0000 Subject: [PATCH] added comments, fixed history, added loadList to browser --- helm/matita/matita.conf.xml | 6 +- helm/matita/matita.glade | 1603 +++++++++++++++------------- helm/matita/matita.ml | 15 +- helm/matita/matita.txt | 3 + helm/matita/matitaEngine.ml | 41 +- helm/matita/matitaGtkMisc.ml | 3 + helm/matita/matitaGtkMisc.mli | 5 + helm/matita/matitaGui.ml | 87 +- helm/matita/matitaGui.mli | 6 +- helm/matita/matitaMathView.ml | 268 +++-- helm/matita/matitaMathView.mli | 5 +- helm/matita/matitaMisc.ml | 25 +- helm/matita/matitaMisc.mli | 2 + helm/matita/matitaScript.ml | 277 +++-- helm/matita/matitaScript.mli | 1 + helm/matita/matitaTypes.ml | 31 +- helm/matita/tests/test4.ma | 19 +- helm/matita/tests/test_instance.ma | 20 +- 18 files changed, 1423 insertions(+), 994 deletions(-) diff --git a/helm/matita/matita.conf.xml b/helm/matita/matita.conf.xml index 54f608692..07887c6bd 100644 --- a/helm/matita/matita.conf.xml +++ b/helm/matita/matita.conf.xml @@ -8,10 +8,10 @@ gares
- localhost - + + mowgli.cs.unibo.it helm - mowgli + matita
true diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade index 2704d164d..57ce4006a 100644 --- a/helm/matita/matita.glade +++ b/helm/matita/matita.glade @@ -79,13 +79,13 @@ Copyright (C) 2005, - 500 - 500 True Cic browser GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE + GTK_WIN_POS_CENTER_ON_PARENT False + 500 + 500 True False True @@ -107,26 +107,29 @@ Copyright (C) 2005, 0 - + True + 0 + 0.5 GTK_SHADOW_OUT - GTK_POS_LEFT - GTK_POS_TOP - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - + True - True - True - False + False + 0 @@ -135,7 +138,7 @@ Copyright (C) 2005, True True GTK_RELIEF_NONE - True + False @@ -149,20 +152,12 @@ Copyright (C) 2005, + + 0 + False + False + - - - False - False - - - - - - True - True - True - False @@ -233,20 +228,12 @@ Copyright (C) 2005, + + 0 + False + False + - - - False - False - - - - - - True - True - True - False @@ -269,20 +256,12 @@ Copyright (C) 2005, + + 0 + False + False + - - - False - False - - - - - - True - True - True - False @@ -305,20 +284,12 @@ Copyright (C) 2005, + + 0 + False + False + - - - False - False - - - - - - True - True - True - False @@ -341,23 +312,15 @@ Copyright (C) 2005, + + 0 + False + False + - - - False - False - - - - - - True - True - True - False - + True gtk-jump-to 4 @@ -366,26 +329,20 @@ Copyright (C) 2005, 0 0 + + 3 + False + False + - - - False - False - - - - - - True - True - True - False True cic uri + True True + True True True 0 @@ -393,14 +350,92 @@ Copyright (C) 2005, True * False - 34 + + 3 + True + True + + + + + + 20 + True + False + 0 + + + + + + + + + + + 0 + False + True + + + + + + True + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_RELIEF_NONE + True + False + False + + + + True + False + 0 + + + + True + GTK_ARROW_DOWN + GTK_SHADOW_NONE + 0.5 + 0.5 + 0 + 0 + + + 0 + True + True + + + + + + + 0 + False + False + - - False - False - @@ -413,83 +448,232 @@ Copyright (C) 2005, - + + 3 True - 0 - 0 - GTK_SHADOW_IN + False + 6 - + True True - GTK_POLICY_AUTOMATIC - GTK_POLICY_AUTOMATIC - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT + True + True + 0 + + True + * + False + + + 0 + True + True + + + + + + True + False + 0 - + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 + + + + + + + 0 + False + False + + + 0 + False + True + 0 - True + False True - - - - - - - - DUMMY - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False - False - True - False - False - GDK_WINDOW_TYPE_HINT_DIALOG - GDK_GRAVITY_NORTH_WEST - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - + True - True - True - gtk-cancel - True - GTK_RELIEF_NORMAL - True - -6 - - + 0 + 0 + GTK_SHADOW_NONE - - - True - True - True - gtk-ok + + + True + True + True + True + GTK_POS_TOP + False + False + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + False + True + + + + + + True + MathView + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + + True + True + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + False + True + + + + + + True + WhelpResults + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + tab + + + + + + + 0 + True + True + + + + + + + + + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + False + False + GDK_WINDOW_TYPE_HINT_DIALOG + GDK_GRAVITY_NORTH_WEST + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + True + -6 + + + + + + True + True + True + gtk-ok True GTK_RELIEF_NORMAL True @@ -1037,698 +1221,612 @@ Copyright (C) 2005, + 2 True GTK_SHADOW_OUT GTK_POS_TOP - GTK_POS_TOP + GTK_POS_LEFT - - 109 + True - True - 0 + 17 + 2 + False + 4 + 0 - + + 50 True - False - 0 - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 55 - True - Intros - True - intros - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Apply - True - apply - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - - - - - True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 55 - True - Exact - True - exact - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - 0 - False - False - - + Apply + True + apply + True + GTK_RELIEF_NORMAL + True - 0 - False - False + 1 + 2 + 0 + 1 + fill + - + + 55 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + Intros + True + intros + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 0 + 1 + fill + + + - - - True - True - True - False + + + 55 + True + Exact + True + exact + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 2 + 3 + fill + + + - - - 55 - True - Elim - True - elim - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + 55 + True + Elim + True + elim + True + GTK_RELIEF_HALF + True + + + 0 + 1 + 4 + 5 + fill + + + - - - True - True - True - False + + + 55 + True + Reflexivity + True + refl + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 8 + 9 + fill + + + - - - 55 - True - ElimType - True - elimTy - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + 50 + True + Symmetry + True + sym + True + GTK_RELIEF_NORMAL + True - 0 - False - False + 1 + 2 + 8 + 9 + fill + - + + 55 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + Transitivity + True + trans + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 9 + 10 + fill + + + - - - True - True - True - False + + + 55 + True + Simplify + True + simpl + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 11 + 12 + fill + + + - - - 25 - True - Split - True - ∧ - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + 50 + True + Reduce + True + red + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 11 + 12 + fill + + + - - - True - True - True - False + + + 55 + True + Whd + True + whd + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 12 + 13 + fill + + + - - - 25 - True - Left - True - L - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + 55 + True + Assumption + True + assum + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 14 + 15 + fill + + + - - - True - True - True - False + + + 50 + True + Auto + True + auto + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 14 + 15 + fill + + + - - - 25 - True - Right - True - R - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + 55 + True + Cut + True + cut + True + GTK_RELIEF_NORMAL + True + + + 0 + 1 + 16 + 17 + fill + + + - - - True - True - True - False + + + 50 + True + Replace + True + repl + True + GTK_RELIEF_NORMAL + True + + + 1 + 2 + 16 + 17 + fill + + + - - - 25 - True - Exists - True - ∃ - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + + + 55 + True + ElimType + True + elimTy + True + GTK_RELIEF_NORMAL + True - 0 - False - False + 1 + 2 + 4 + 5 + fill + - + True False 0 - + + 25 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 55 - True - Reflexivity - True - refl - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Symmetry - True - sym - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + Right + True + R + True + GTK_RELIEF_NORMAL + True 0 - False - False + True + True - + + 25 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 55 - True - Transitivity - True - trans - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + Exists + True + ∃ + True + GTK_RELIEF_NORMAL + True 0 - False - False + True + True - 0 - False - False + 1 + 2 + 6 + 7 + fill + fill - + True False 0 - + + 25 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 55 - True - Simplify - True - simpl - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - - - - - True - True - True - False - - - - 50 - True - Reduce - True - red - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + Split + True + ∧ + True + GTK_RELIEF_NORMAL + True 0 - False - False + True + True - + + 25 True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True - - - - True - True - True - False - - - - 55 - True - Whd - True - whd - True - GTK_RELIEF_NORMAL - True - - - - - False - False - - + Left + True + L + True + GTK_RELIEF_NORMAL + True 0 - False - False + True + True - 0 - False - False + 0 + 1 + 6 + 7 + fill + fill - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - True - True - True - False - - - - 55 - True - Assumption - True - assum - True - GTK_RELIEF_NORMAL - True - - - - - False - False - + + + + 0 + 1 + 1 + 2 + fill + + + + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - True - True - True - False + + + + + 0 + 1 + 3 + 4 + fill + + - - - 50 - True - Auto - True - auto - True - GTK_RELIEF_NORMAL - True - - - - - False - False - + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 + + + - 0 - False - False + 0 + 1 + 5 + 6 + fill - + True - GTK_ORIENTATION_HORIZONTAL - GTK_TOOLBAR_BOTH - True - True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - True - True - True - False + + + + + 0 + 1 + 7 + 8 + fill + + - - - 55 - True - Cut - True - cut - True - GTK_RELIEF_NORMAL - True - - - - - False - False - + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 + + + + + + 0 + 1 + 10 + 11 + fill + + + + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 - - True - True - True - False + + + + + 0 + 1 + 13 + 14 + fill + + - - - 50 - True - Replace - True - repl - True - GTK_RELIEF_NORMAL - True - - - - - False - False - + + + True + 0.5 + 0.5 + 1 + 1 + 0 + 0 + 0 + 0 + + + - 0 - False - False + 0 + 1 + 15 + 16 + fill @@ -1736,7 +1834,7 @@ Copyright (C) 2005, 0 - True + False True @@ -2166,7 +2264,7 @@ Copyright (C) 2005, True - True + False 0 @@ -2440,7 +2538,7 @@ Copyright (C) 2005, True False - 0 + 4 @@ -2546,7 +2644,19 @@ Copyright (C) 2005, - + + True + True + gtk-copy + True + GTK_RELIEF_NORMAL + True + 0 + + + + + True True True @@ -2555,7 +2665,7 @@ Copyright (C) 2005, 0 - + True 0.5 0.5 @@ -2567,13 +2677,13 @@ Copyright (C) 2005, 0 - + True False 2 - + True gtk-ok 4 @@ -2590,9 +2700,9 @@ Copyright (C) 2005, - + True - _Auto + bla bla bla True False GTK_JUSTIFY_LEFT @@ -2628,7 +2738,7 @@ Copyright (C) 2005, True False - 0 + 3 @@ -2653,10 +2763,11 @@ Copyright (C) 2005, + 400 True True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS + GTK_POLICY_AUTOMATIC + GTK_POLICY_AUTOMATIC GTK_SHADOW_NONE GTK_CORNER_TOP_LEFT @@ -2679,7 +2790,7 @@ Copyright (C) 2005, - + True False 0 diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index 3f08dd1c8..cf7939fa7 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -63,6 +63,15 @@ let script = ~buffer:gui#main#scriptTextView#buffer ~init:(Lazy.force MatitaEngine.initial_status) ~mathviewer:(MatitaMathView.mathViewer ()) + ~urichooser:(fun uris -> + try + MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE + ~title:"Matita: URI chooser" + ~msg:"Select the URI" ~hide_uri_entry:true + ~hide_try:true ~ok_label:"_Apply" + ~copy_cb:(fun s -> gui#main#scriptTextView#buffer#insert ("\n"^s^"\n")) + () ~id:"boh?" uris + with MatitaTypes.Cancel -> []) () (* math viewers *) @@ -70,7 +79,7 @@ let _ = let sequent_viewer = MatitaMathView.sequentViewer_instance () in let sequents_viewer = MatitaMathView.sequentsViewer_instance () in sequent_viewer#set_href_callback - (Some (fun uri -> (MatitaMathView.cicBrowser ())#loadUri uri)); + (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri uri))); let browser_observer _ = MatitaMathView.refresh_all_browsers () in let sequents_observer status = sequents_viewer#reset; @@ -149,13 +158,13 @@ let _ = print_endline "\nThanks for using Matita!\n"); Sys.catch_break true; (try - script#loadFrom Sys.argv.(1); + gui#loadScript Sys.argv.(1); with Invalid_argument _ -> ()); if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *) Helm_registry.set "matita.mode" "cicbrowser"; let browser = MatitaMathView.cicBrowser () in try - browser#loadUri Sys.argv.(1) + browser#load (`Uri Sys.argv.(1)) with Invalid_argument _ -> () end else begin (* matita *) Helm_registry.set "matita.mode" "matita"; diff --git a/helm/matita/matita.txt b/helm/matita/matita.txt index 30a8b5355..62f133675 100644 --- a/helm/matita/matita.txt +++ b/helm/matita/matita.txt @@ -12,6 +12,9 @@ TODO - spostare il codice di creazione delle tabelle da MatitaDb, al momento quelle create da matita possono andare out of sync con quelle create dai file .sql +- commenti exeguibili (forse devono essere una lista e non + un singolo executable e forse devono contenere anche Note + e non solo Executable DONE - tree update in background -> Gares diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 59d1c7b79..437fed32d 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -57,8 +57,12 @@ let tactic_of_ast = function | TacticAst.LetIn of 'term * 'ident | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option *) + | TacticAst.Rewrite (_,dir,t,ident) -> + if dir = `Left then + EqualityTactics.rewrite_tac ~term:t + else + EqualityTactics.rewrite_back_tac ~term:t | _ -> assert false let eval_tactical status tac = @@ -200,14 +204,21 @@ let eval_command status cmd = (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases } -let eval status st = - match st with +let eval_executable status ex = + match ex with | TacticAst.Tactical (_, tac) -> eval_tactical status tac | TacticAst.Command (_, cmd) -> eval_command status cmd | TacticAst.Macro (_, mac) -> command_error (sprintf "The macro %s can't be in a script" (TacticAstPp.pp_macro_cic mac)) +let eval_comment status c = status + +let eval status st = + match st with + | TacticAst.Executable (_,ex) -> eval_executable status ex + | TacticAst.Comment (_,c) -> eval_comment status c + let disambiguate_term status term = let (aliases, metasenv, cic, _) = match @@ -283,8 +294,10 @@ let disambiguate_tactic status = function | TacticAst.LetIn of 'term * 'ident | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option | TacticAst.Replace_pattern of 'term pattern * 'term - | TacticAst.Rewrite of direction * 'term * 'ident option *) + | TacticAst.Rewrite (loc,dir,t,ident) -> + let status, term = disambiguate_term status t in + status, TacticAst.Rewrite (loc,dir,term,ident) | TacticAst.Intros (loc, num, names) -> status, TacticAst.Intros (loc, num, names) | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num) @@ -430,8 +443,8 @@ let disambiguate_command status = function status, cmd | TacticAst.Alias _ as x -> status, x -let disambiguate_statement status statement = - match statement with +let disambiguate_executable status ex = + match ex with | TacticAst.Tactical (loc, tac) -> let status, tac = disambiguate_tactical status tac in status, (TacticAst.Tactical (loc, tac)) @@ -442,6 +455,22 @@ let disambiguate_statement status statement = command_error (sprintf ("The engine is not allowed to disambiguate any macro, "^^ "in particular %s") (TacticAstPp.pp_macro_ast mac)) + +let disambiguate_comment status c = + match c with + | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n) + | TacticAst.Code (loc,ex) -> + let status, ex = disambiguate_executable status ex in + status, TacticAst.Code (loc,ex) + +let disambiguate_statement status statement = + match statement with + | TacticAst.Comment (loc,c) -> + let status, c = disambiguate_comment status c in + status, TacticAst.Comment (loc,c) + | TacticAst.Executable (loc,ex) -> + let status, ex = disambiguate_executable status ex in + status, TacticAst.Executable (loc,ex) let eval_ast status ast = let status,st = disambiguate_statement status ast in diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 274ee123a..0301b31f2 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -39,6 +39,9 @@ let wrap_callback f () = let connect_button (button: #GButton.button) callback = ignore (button#connect#clicked (wrap_callback callback)) +let connect_toggle_button (button: #GButton.toggle_button) callback = + ignore (button#connect#toggled (wrap_callback callback)) + let connect_menu_item (menu_item: #GMenu.menu_item) callback = ignore (menu_item#connect#activate (wrap_callback callback)) diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli index 23f820f86..993dff4c3 100644 --- a/helm/matita/matitaGtkMisc.mli +++ b/helm/matita/matitaGtkMisc.mli @@ -39,6 +39,11 @@ val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit * value *) val connect_button: #GButton.button -> (unit -> unit) -> unit + +(** Connect a callback to the toggled signal of a button, ignoring its return + * value *) +val connect_toggle_button: #GButton.toggle_button -> (unit -> unit) -> unit + (** Like connect_button above, but connects a callback to the activate signal of * a menu item *) val connect_menu_item: #GMenu.menu_item -> (unit -> unit) -> unit diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index ec4d042ff..5045f36d1 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -63,7 +63,8 @@ class gui () = object (self) val mutable chosen_file = None val mutable _ok_not_exists = false - + val mutable script_fname = None + initializer (* glade's check widgets *) List.iter (fun w -> w#check_widgets ()) @@ -155,33 +156,37 @@ class gui () = (sprintf "Uncaught exception: %s" (Printexc.to_string exn))); (* script *) let s () = MatitaScript.instance () in - let script_fname = ref None in - let enable_save_to f = - script_fname := Some f; - self#main#saveMenuItem#misc#set_sensitive true - in - let disable_save () = - script_fname := None; + let disableSave () = + script_fname <- None; self#main#saveMenuItem#misc#set_sensitive false in let loadScript () = let script = s () in match self#chooseFile () with - | Some f -> script#reset (); script#loadFrom f; enable_save_to f + | Some f -> + script#reset (); + script#loadFrom f; + console#message ("'"^f^"' loaded."); + self#_enableSaveTo f | None -> () in let saveAsScript () = let script = s () in match self#chooseFile ~ok_not_exists:true () with - | Some f -> script#saveTo f; enable_save_to f + | Some f -> + script#saveTo f; + console#message ("'"^f^"' saved."); + self#_enableSaveTo f | None -> () in let saveScript () = - match !script_fname with + match script_fname with | None -> saveAsScript () - | Some f -> (s ())#saveTo f + | Some f -> + (s ())#saveTo f; + console#message ("'"^f^"' saved."); in - let newScript () = (s ())#reset (); disable_save () in + let newScript () = (s ())#reset (); disableSave () in let cursor () = let buf = self#main#scriptTextView#buffer in buf#place_cursor (buf#get_iter_at_mark (`NAME "locked")) @@ -228,6 +233,18 @@ class gui () = self#main#hintHighImage#set_file "icons/matita-bulb-high.png"; (* focus *) self#main#scriptTextView#misc#grab_focus () + + method loadScript file = + let script = MatitaScript.instance () in + script#reset (); + script#loadFrom file; + console#message ("'"^file^"' loaded."); + self#_enableSaveTo file + + method private _enableSaveTo file = + script_fname <- Some file; + self#main#saveMenuItem#misc#set_sensitive true + method console = console @@ -237,6 +254,30 @@ class gui () = method newBrowserWin () = let win = new browserWin () in + win#whelpImage2#set_file "icons/whelp.png"; + win#whelpBarToggleButton#set_active false; + win#whelpBarBox#misc#hide (); + win#mathOrListNotebook#set_show_tabs false; + connect_toggle_button win#whelpBarToggleButton + (fun () -> + if win#whelpBarToggleButton#active then + win#whelpBarBox#misc#show () + else + win#whelpBarBox#misc#hide ()); + let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in + let combo,(combo_store,combo_column) = + GEdit.combo_box_text ~strings:queries () + in + combo#set_active 0; + win#comboVbox#add (combo :> GObj.widget); + let start_query () = + let query = String.lowercase (List.nth queries combo#active) in + let input = win#queryInputText#text in + let statement = "whelp " ^ query ^ " " ^ input ^ "." in + (MatitaScript.instance ())#advance ~statement () + in + ignore(win#queryInputText#connect#activate ~callback:start_query); + ignore(combo#connect#changed ~callback:start_query); win#check_widgets (); win @@ -312,7 +353,8 @@ let is_var_uri s = let interactive_uri_choice ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "") - ?(msg = "") ?(nonvars_button = false) () + ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) + ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb () ~id uris = let gui = instance () in @@ -323,11 +365,28 @@ let interactive_uri_choice Lazy.force nonvars_uris else begin let dialog = gui#newUriDialog () in + if hide_uri_entry then + dialog#uriEntryHBox#misc#hide (); + if hide_try then + begin + dialog#uriChoiceSelectedButton#misc#hide (); + dialog#uriChoiceConstantsButton#misc#hide (); + end; + dialog#okLabel#set_label ok_label; dialog#uriChoiceTreeView#selection#set_mode (selection_mode :> Gtk.Tags.selection_mode); let model = new stringListModel dialog#uriChoiceTreeView in let choices = ref None in let nonvars = ref false in + (match copy_cb with + | None -> () + | Some cb -> + dialog#copyButton#misc#show (); + connect_button dialog#copyButton + (fun _ -> + match model#easy_selection () with + | [u] -> (cb u) + | _ -> ())); dialog#uriChoiceDialog#set_title title; dialog#uriChoiceLabel#set_text msg; List.iter model#easy_append uris; diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli index aabcba1e8..cb2cbeb0c 100644 --- a/helm/matita/matitaGui.mli +++ b/helm/matita/matitaGui.mli @@ -69,6 +69,8 @@ object (** prompt the user for a (multiline) text entry *) method askText: ?title:string -> ?msg:string -> unit -> string option + method loadScript: string -> unit + end (** singleton instance of the gui *) @@ -84,7 +86,9 @@ val instance: unit -> gui * @raise MatitaTypes.Cancel *) val interactive_uri_choice: ?selection_mode:([`SINGLE|`MULTIPLE]) -> ?title:string -> - ?msg:string -> ?nonvars_button:bool -> unit -> + ?msg:string -> ?nonvars_button:bool -> + ?hide_uri_entry:bool -> ?hide_try:bool -> ?ok_label:string -> + ?copy_cb:(string -> unit) -> unit -> MatitaDisambiguator.choose_uris_callback (** @raise MatitaTypes.Cancel *) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index c9e0b217f..1f18e76a6 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -280,11 +280,14 @@ let cicBrowsers = ref [] class type cicBrowser = object - method loadUri: string -> unit - method loadTerm: term_source -> unit + method load: MatitaTypes.mathViewer_entry -> unit + method loadList: string list -> MatitaTypes.mathViewer_entry-> unit + method loadInput: string -> unit end -class cicBrowser_impl ~(history:string MatitaMisc.history) () = +class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) + () += let term_RE = Pcre.regexp "^term:(.*)" in let trailing_slash_RE = Pcre.regexp "/$" in let gui = MatitaGui.instance () in @@ -306,10 +309,12 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () = inherit scriptAccessor initializer + win#browserForwardButton#misc#set_sensitive false; + win#browserBackButton#misc#set_sensitive false; ignore (win#browserUri#connect#activate (handle_error' (fun () -> - self#_loadUri win#browserUri#text))); + self#loadInput win#browserUri#text))); ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> - self#_loadUri current_proof_uri))); + self#_load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked (handle_error' self#refresh)); ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); @@ -323,107 +328,139 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () = then GMain.quit (); false)); + ignore(win#whelpResultTreeview#connect#row_activated + ~callback:(fun _ _ -> + let old = win#browserUri#text in + self#loadInput (old ^ self#_getWhelpResultTreeviewSelection ()))); mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#_loadUri uri))); - self#_loadUri ~add_to_history:false blank_uri; - toplevel#show (); + handle_error (fun () -> self#_load (`Uri uri)))); + self#_load (`About `Blank); + toplevel#show () - val mutable current_uri = "" + val mutable current_entry = `About `Blank val mutable current_infos = None val mutable current_mathml = None + val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview + + method private _getWhelpResultTreeviewSelection () = + match model#easy_selection () with + | [u] -> u + | _ -> assert false + + (** history RATIONALE + * + * all operations about history are done using _historyFoo + * + * only toplevel function like load loadList loadInput can call + * _historyAdd + *) + + method private _historyAdd item = + history#add item; + win#browserBackButton#misc#set_sensitive true; + win#browserForwardButton#misc#set_sensitive false + + method private _historyPrev () = + let item = history#previous in + if history#is_begin then win#browserBackButton#misc#set_sensitive false; + win#browserForwardButton#misc#set_sensitive true; + item + + method private _historyNext () = + let item = history#next in + if history#is_end then win#browserForwardButton#misc#set_sensitive false; + win#browserBackButton#misc#set_sensitive true; + item + + (** notebook RATIONALE + * + * Use only these functions to switch between the tabs + *) + method private _showList = win#mathOrListNotebook#goto_page 1 + method private _showMath = win#mathOrListNotebook#goto_page 0 + + + method private back () = try - self#_loadUri ~add_to_history:false history#previous + self#_load (self#_historyPrev ()) with MatitaMisc.History_failure -> () method private forward () = try - self#_loadUri ~add_to_history:false history#next + self#_load (self#_historyNext ()) with MatitaMisc.History_failure -> () (* loads a uri which can be a cic uri or an about:* uri * @param uri string *) - method private _loadUri ?(add_to_history = true) uri = + method private _load entry = try - if current_uri <> uri || uri = current_proof_uri then begin - (match uri with - | uri when uri = blank_uri -> self#blank () - | uri when uri = current_proof_uri -> self#home () - | uri when Pcre.pmatch ~rex:term_RE uri -> - self#loadTerm (`String (Pcre.extract ~rex:term_RE uri).(1)) - | uri when Pcre.pmatch ~rex:trailing_slash_RE uri -> self#loadDir uri - | _ -> self#loadUriManagerUri (UriManager.uri_of_string uri)); - self#setUri uri; - if add_to_history then history#add uri - end + if entry <> current_entry || entry = `About `Current_proof then begin + (match entry with + | `About `Current_proof -> self#home () + | `About `Blank -> self#blank () + | `About `Us -> () (* TODO implement easter egg here :-] *) + | `Check term -> self#_loadCheck term + | `Cic (term, metasenv) -> self#_loadTermCic term metasenv + | `Dir dir -> self#_loadDir dir + | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri) + | `Whelp (query, results) -> self#loadList results entry); + self#setEntry entry + end with - | UriManager.IllFormedUri _ -> fail (sprintf "invalid uri: %s" uri) - | CicEnvironment.Object_not_found _ -> - fail (sprintf "object not found: %s" uri) + | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri) + | CicEnvironment.Object_not_found uri -> + fail (sprintf "object not found: %s" (UriManager.string_of_uri uri)) | Browser_failure msg -> fail msg - method loadUri uri = - handle_error (fun () -> self#_loadUri ~add_to_history:true uri) method private blank () = - mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement + mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement; + self#_showMath + + method private _loadCheck term = + failwith "not implemented _loadCheck"; + self#_showMath method private home () = + self#_showMath; match self#script#status.proof_status with | Proof (uri, metasenv, bo, ty) -> let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in - self#loadObj obj + self#_loadObj obj | Incomplete_proof ((uri, metasenv, bo, ty), _) -> let name = UriManager.name_of_uri (MatitaMisc.unopt uri) in let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], []) in - self#loadObj obj + self#_loadObj obj | _ -> self#blank () (** loads a cic uri from the environment * @param uri UriManager.uri *) - method private loadUriManagerUri uri = + method private _loadUriManagerUri uri = let uri = UriManager.strip_xpointer uri in let (obj, _) = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - self#loadObj obj - - method private loadDir dir = - let mathml = MatitaMisc.empty_boxml () in + self#_loadObj obj + + method private _loadDir dir = let content = Http_getter.ls dir in - let root = mathml#get_documentElement in - let new_box_elt name = - mathml#createElementNS ~namespaceURI:(Some Misc.boxml_ns) - ~qualifiedName:(Gdome.domString ("b:" ^ name)) + let l = List.map (function + | Http_getter_types.Ls_section sec -> sec + | Http_getter_types.Ls_object obj -> obj.Http_getter_types.uri + ) content in - let new_text content = mathml#createTextNode (Gdome.domString content) in - let b_v = new_box_elt "v" in - List.iter - (fun item -> - let b_text = new_box_elt "text" in - let uri, elt = - match item with - | Http_getter_types.Ls_section subdir -> - (dir ^ subdir ^ "/"), (new_text (subdir ^ "/")) - | Http_getter_types.Ls_object obj -> - (dir ^ obj.Http_getter_types.uri), - (new_text obj.Http_getter_types.uri) - in - b_text#setAttributeNS ~namespaceURI:(Some Misc.xlink_ns) - ~qualifiedName:(Gdome.domString "xlink:href") - ~value:(Gdome.domString uri); - ignore (b_v#appendChild ~newChild:(b_text :> Gdome.node)); - ignore (b_text#appendChild ~newChild:(elt :> Gdome.node))) - content; - ignore (root#appendChild ~newChild:(b_v :> Gdome.node)); -(* Misc.domImpl#saveDocumentToFile ~doc:mathml ~name:"pippo" (); *) - mathView#load_root ~root:root - - method private setUri uri = - win#browserUri#set_text uri; - current_uri <- uri - - method private loadObj obj = + self#_loadList l + + method private setEntry entry = + win#browserUri#set_text (string_of_entry entry); + current_entry <- entry + + method private _loadObj obj = + self#_showMath; + (* this must be _before_ loading the document, since + * if the widget is not mapped (hidden by the notebook) + * the document is not rendered *) let use_diff = false in (* ZACK TODO use XmlDiff when re-rendering? *) let (mathml, (_,(ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,_,_))) = @@ -431,51 +468,69 @@ class cicBrowser_impl ~(history:string MatitaMisc.history) () = in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses); - match current_mathml with + (match current_mathml with | Some current_mathml when use_diff -> mathView#freeze; XmlDiff.update_dom ~from:current_mathml mathml; mathView#thaw | _ -> mathView#load_root ~root:mathml#get_documentElement; - current_mathml <- Some mathml - - method private _loadTerm s = failwith "not implemented _loadTerm" -(* TODO self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s)) *) - - method private _loadTermAst ast = failwith "not implemented _loadTermAst" -(* TODO - let (_, metasenv, term, _) = - MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast - in - self#_loadTermCic term metasenv -*) + current_mathml <- Some mathml); method private _loadTermCic term metasenv = let context = self#script#proofContext in let dummyno = CicMkImplicit.new_meta metasenv [] in let sequent = (dummyno, context, term) in - mathView#load_sequent (sequent :: metasenv) dummyno - - method loadTerm (src:term_source) = - handle_error (fun () -> - (match src with - | `Ast ast -> self#_loadTermAst ast - | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv - | `String s -> self#_loadTerm s); - self#setUri "check") - + mathView#load_sequent (sequent :: metasenv) dummyno; + self#_showMath + + method private _loadList l = + model#list_store#clear (); + List.iter model#easy_append l; + self#_showList + + (** { public methods } *) + + method load uri = + handle_error (fun () -> self#_load uri); + self#_historyAdd uri + + method loadList l entry = + self#_loadList l; + self#_historyAdd entry + + method loadInput txt = + let add_terminating_slash s = + if s.[String.length s - 1] <> '/' then s^"/" else s + in + let is_uri = + try + ignore(Http_getter.resolve txt); true + with + | Http_getter_types.Key_not_found _ + | Http_getter_types.Unresolvable_URI _ -> false + in + let entry = + if is_uri then + (`Uri txt) + else + (`Dir (add_terminating_slash txt)) + in + self#_load entry; + self#_historyAdd entry + + (** {2 methods used by constructor only} *) method win = win method history = history - method currentUri = current_uri + method currentEntry = current_entry method refresh () = - if current_uri = current_proof_uri then - self#_loadUri ~add_to_history:false current_proof_uri - + if current_entry = `About `Current_proof then + self#_load (`About `Current_proof) end + let sequentsViewer ~(notebook:GPack.notebook) ~(sequentViewer:sequentViewer) () = @@ -488,10 +543,11 @@ let cicBrowser () = let win = browser#win in ignore (win#browserNewButton#connect#clicked (fun () -> let history = - new MatitaMisc.browser_history ~memento:history#save size "" + new MatitaMisc.browser_history ~memento:history#save size + (`About `Blank) in let newBrowser = aux history in - newBrowser#loadUri browser#currentUri)); + newBrowser#load browser#currentEntry)); (* (* attempt (failed) to close windows on CTRL-W ... *) MatitaGtkMisc.connect_key win#browserWinEventBox#event ~modifiers:[`CONTROL] @@ -500,7 +556,7 @@ let cicBrowser () = cicBrowsers := browser :: !cicBrowsers; (browser :> cicBrowser) in - let history = new MatitaMisc.browser_history size blank_uri in + let history = new MatitaMisc.browser_history size (`About `Blank) in aux history let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers @@ -514,8 +570,18 @@ let default_sequentsViewer () = sequentsViewer ~notebook:gui#main#sequentsNotebook ~sequentViewer () let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer - let mathViewer () = - object - method show_term t = (cicBrowser ()) # loadTerm t + object(self) + method private get_browser reuse = + if reuse then + (match !cicBrowsers with + | [] -> cicBrowser () + | b :: _ -> (b :> cicBrowser)) + else + (cicBrowser ()) + + method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t + + method show_uri_list ?(reuse=false) ~entry l = + (self#get_browser reuse)#loadList l entry end diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index e26352dad..1dc3dabe8 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -62,8 +62,9 @@ exception Browser_failure of string class type cicBrowser = object - method loadUri: string -> unit - method loadTerm: MatitaTypes.term_source -> unit + method load: MatitaTypes.mathViewer_entry -> unit + method loadList: string list -> MatitaTypes.mathViewer_entry -> unit + method loadInput: string -> unit end (** {2 Constructors} *) diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index 41b967938..e1c55feb2 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -76,17 +76,30 @@ class type ['a] history = method previous : 'a method load: 'a memento -> unit method save: 'a memento + method is_begin: bool + method is_end: bool end +class basic_history (head, tail, cur) = + object + val mutable hd = head (* insertion point *) + val mutable tl = tail (* oldest inserted item *) + val mutable cur = cur (* current item for the history *) + + method is_begin = cur <= tl + method is_end = cur >= hd + end + + class shell_history size = let size = size + 1 in let decr x = let x' = x - 1 in if x' < 0 then size + x' else x' in let incr x = (x + 1) mod size in object (self) val data = Array.create size "" - val mutable hd = 0 (* insertion point *) - val mutable tl = -1 (* oldest inserted item *) - val mutable cur = -1 (* current item for the history *) + + inherit basic_history (0, -1 , -1) + method add s = data.(hd) <- s; if tl = -1 then tl <- hd; @@ -112,9 +125,9 @@ class ['a] browser_history ?memento size init = object (self) initializer match memento with Some m -> self#load m | _ -> () val data = Array.create size init - val mutable hd = 0 - val mutable tl = 0 - val mutable cur = 0 + + inherit basic_history (0, 0, 0) + method previous = if cur = tl then raise History_failure; cur <- cur - 1; diff --git a/helm/matita/matitaMisc.mli b/helm/matita/matitaMisc.mli index 4f2905a24..3731bd1a6 100644 --- a/helm/matita/matitaMisc.mli +++ b/helm/matita/matitaMisc.mli @@ -59,6 +59,8 @@ class type ['a] history = method previous : 'a (** @raise History_failure *) method load: 'a memento -> unit method save: 'a memento + method is_begin: bool + method is_end: bool end (** shell like history: new items added at the end of the history diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index c64653c79..fed62fbb3 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -34,8 +34,16 @@ let safe_substring s i j = try String.sub s i j with Invalid_argument _ -> assert false let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*" -let blanks_RE = Pcre.regexp "^\\s*$" - +let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" +let multiline_RE = Pcre.regexp "^\n[^\n]+$" +let newline_RE = Pcre.regexp "\n" + +let comment str = + if Pcre.pmatch ~rex:multiline_RE str then + "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " **)" + else + "\n(**\n" ^ str ^ "\n**)" + let first_line s = let s = Pcre.replace ~rex:heading_nl_RE s in try @@ -53,109 +61,173 @@ let prepend_text header base = let goal_ast n = let module A = TacticAst in let loc = CicAst.dummy_floc in - A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n))) - -let eval_statement status mathviewer user_goal s = - let st = CicTextualParser2.parse_statement (Stream.of_string s) in - match st with - | TacticAst.Command (loc, _) | TacticAst.Tactical (loc, _) -> - let parsed_text_length = snd (CicAst.loc_of_floc loc) in - let parsed_text = safe_substring s 0 parsed_text_length in - let goal_changed = ref false in - let status = - match status.proof_status with - | Incomplete_proof (_, goal) when goal <> user_goal -> - goal_changed := true; - MatitaEngine.eval_ast status (goal_ast user_goal) - | _ -> status - in - let new_status = MatitaEngine.eval_ast status st in - let new_aliases = - match st with - | TacticAst.Command (_, TacticAst.Alias _) -> - DisambiguateTypes.Environment.empty - | _ -> MatitaSync.alias_diff ~from:status new_status - in - let new_text = - if DisambiguateTypes.Environment.is_empty new_aliases then - parsed_text - else - prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases) - parsed_text - in - let new_text = - if !goal_changed then - prepend_text - (TacticAstPp.pp_tactic (TacticAst.Goal (loc, user_goal))(* ^ "\n"*)) - new_text - else - new_text + A.Executable (loc, A.Tactical (loc, A.Tactic (loc, A.Goal (loc, n)))) + +let eval_with_engine status user_goal parsed_text st = + let module TA = TacticAst in + let module TAPp = TacticAstPp in + let parsed_text_length = String.length parsed_text in + let loc, ex = + match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false + in + let goal_changed = ref false in + let status = + match status.proof_status with + | Incomplete_proof (_, goal) when goal <> user_goal -> + goal_changed := true; + MatitaEngine.eval_ast status (goal_ast user_goal) + | _ -> status + in + let new_status = MatitaEngine.eval_ast status st in + let new_aliases = + match ex with + | TA.Command (_, TA.Alias _) -> + DisambiguateTypes.Environment.empty + | _ -> MatitaSync.alias_diff ~from:status new_status + in + let new_text = + if DisambiguateTypes.Environment.is_empty new_aliases then + parsed_text + else + prepend_text (CicTextualParser2.EnvironmentP3.to_string new_aliases) + parsed_text + in + let new_text = + if !goal_changed then + prepend_text + (TAPp.pp_tactic (TA.Goal (loc, user_goal))(* ^ "\n"*)) + new_text + else + new_text + in + [ new_status, new_text ], parsed_text_length + +let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text mac = + let module TA = TacticAst in + let module TAPp = TacticAstPp in + let module MQ = MetadataQuery in + let module MD = MatitaDisambiguator in + let module MDB = MatitaDb in + let parsed_text_length = String.length parsed_text in + match mac with + | TA.Hint loc -> + let s = MatitaMisc.get_proof_status status in + let l = List.map fst (MQ.experimental_hint ~dbd:(MDB.instance ()) s) in + let selected = urichooser l in + (match selected with + | [] -> [], parsed_text_length + | [uri] -> + let ast = + (TA.Executable (loc, + (TA.Tactical (loc, + TA.Tactic (loc, + TA.Apply (loc, CicAst.Uri (uri,None))))))) + in + let new_status = MatitaEngine.eval_ast status ast in + let extra_text = + comment parsed_text ^ + "\n" ^ TAPp.pp_statement ast + in + [ new_status , extra_text ],parsed_text_length + | _ -> assert false) + | TA.Match (_,term) -> + let dbd = MatitaDb.instance () in + let metasenv = MatitaMisc.get_proof_metasenv status in + let context = MatitaMisc.get_proof_context status in + let aliases = MatitaMisc.get_proof_aliases status in + let (_env,_metasenv,term,_graph) = + let interps = + MD.disambiguate_term dbd context metasenv aliases term + in + match interps with + | [x] -> x + | _ -> assert false in - [ new_status, new_text ], parsed_text_length - | TacticAst.Macro (loc, mac) -> - let parsed_text_length = snd (CicAst.loc_of_floc loc) in - (match mac with (* TODO *) - | TacticAst.Hint _ -> - let s = MatitaMisc.get_proof_status status in - let l = List.map fst - (MetadataQuery.experimental_hint ~dbd:(MatitaDb.instance ()) s) - in - List.iter prerr_endline l; - prerr_endline "FINITA LA HINT"; assert false - | TacticAst.Match (_,term) -> - let dbd = MatitaDb.instance () in - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in - let (_env,_metasenv,term,_graph) = - let interps = - MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term - in - match interps with - | [x] -> x - | _ -> assert false + let results = MetadataQuery.match_term ~dbd:dbd term in + mathviewer#show_uri_list ~reuse:true ~entry:(`Whelp ("match", results)) + results; + [], parsed_text_length + | TA.Instance (_,term) -> + let dbd = MatitaDb.instance () in + let metasenv = MatitaMisc.get_proof_metasenv status in + let context = MatitaMisc.get_proof_context status in + let aliases = MatitaMisc.get_proof_aliases status in + let (_env,_metasenv,term,_graph) = + let interps = + MD.disambiguate_term dbd context metasenv aliases term in - List.iter prerr_endline (MetadataQuery.match_term ~dbd:dbd term); - assert false; - | TacticAst.Instance (_,term) -> - let dbd = MatitaDb.instance () in - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in - let (_env,_metasenv,term,_graph) = - let interps = - MatitaDisambiguator.disambiguate_term dbd context metasenv aliases term - in match interps with - | [x] -> x - | _ -> assert false + | [x] -> x + | _ -> assert false + in + let results = MetadataQuery.instance ~dbd term in + mathviewer#show_uri_list ~reuse:true + ~entry:(`Whelp ("instance", results)) results; + [], parsed_text_length + + + | TA.Check (_,t) -> + let metasenv = MatitaMisc.get_proof_metasenv status in + let context = MatitaMisc.get_proof_context status in + let aliases = MatitaMisc.get_proof_aliases status in + let db = MatitaDb.instance () in + let (_env,_metasenv,term,_graph) = + let interps = + MD.disambiguate_term db context metasenv aliases t in - List.iter prerr_endline (MetadataQuery.instance ~dbd term); - assert false - - | TacticAst.Check (_,t) -> - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in - let db = MatitaDb.instance () in - let (_env,_metasenv,term,_graph) = - let interps = - MatitaDisambiguator.disambiguate_term db context metasenv aliases t - in - match interps with - | [x] -> x - | _ -> assert false - in - let ty,_ = - CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph - in - mathviewer # show_term (`Cic (ty,metasenv) ); - [ status, "" ] , parsed_text_length - | _ -> failwith "not implemented") + match interps with + | [x] -> x + | _ -> assert false + in + let ty,_ = + CicTypeChecker.type_of_aux' metasenv context term + CicUniv.empty_ugraph + in + let t_and_ty = Cic.Cast (term,ty) in + mathviewer # show_entry (`Cic (t_and_ty,metasenv)); + [], parsed_text_length + | TA.Quit _ -> + failwith "not implemented quit" + | _ -> failwith "not implemented" + + +let eval_executable status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal parsed_text ex = + let module TA = TacticAst in + let module TAPp = TacticAstPp in + let module MD = MatitaDisambiguator in + let parsed_text_length = String.length parsed_text in + match ex with + | TA.Command (loc, _) | TA.Tactical (loc, _) -> + eval_with_engine status user_goal parsed_text (TA.Executable (loc, ex)) + | TA.Macro (_,mac) -> + eval_macro status mathviewer urichooser parsed_text mac + +let rec eval_statement status (mathviewer:MatitaTypes.mathViewer) urichooser user_goal s = + if Pcre.pmatch ~rex:only_dust_RE s then raise Margin; + let st = CicTextualParser2.parse_statement (Stream.of_string s) in + let text_of_loc loc = + let parsed_text_length = snd (CicAst.loc_of_floc loc) in + let parsed_text = safe_substring s 0 parsed_text_length in + parsed_text, parsed_text_length + in + match st with + | TacticAst.Comment (loc,_)-> + let parsed_text, parsed_text_length = text_of_loc loc in + let remain_len = String.length s - parsed_text_length in + let s = String.sub s parsed_text_length remain_len in + let s,len = eval_statement status mathviewer urichooser user_goal s in + (match s with + | (status, text) :: tl -> + ((status, parsed_text ^ text)::tl), (parsed_text_length + len) + | [] -> [], 0) + | TacticAst.Executable (loc, ex) -> + let parsed_text, parsed_text_length = text_of_loc loc in + eval_executable status mathviewer urichooser user_goal parsed_text ex + class script ~(buffer: GText.buffer) ~(init: MatitaTypes.status) - ~(mathviewer: MatitaTypes.mathViewer) () = + ~(mathviewer: MatitaTypes.mathViewer) + ~urichooser () = object (self) initializer self#reset () @@ -180,10 +252,9 @@ object (self) method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in - if Pcre.pmatch ~rex:blanks_RE s then raise Margin; MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); let (entries, parsed_len) = - eval_statement self#status mathviewer userGoal s in + eval_statement self#status mathviewer urichooser userGoal s in let (new_statuses, new_statements) = List.split entries in (* prerr_endline "evalStatement returned"; @@ -317,8 +388,8 @@ end let _script = ref None -let script ~buffer ~init ~mathviewer () = - let s = new script ~buffer ~init ~mathviewer () in +let script ~buffer ~init ~mathviewer ~urichooser () = + let s = new script ~buffer ~init ~mathviewer ~urichooser () in _script := Some s; s diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli index f7c86fc3c..df3ec4e1e 100644 --- a/helm/matita/matitaScript.mli +++ b/helm/matita/matitaScript.mli @@ -65,6 +65,7 @@ val script: buffer:GText.buffer -> init:MatitaTypes.status -> mathviewer: MatitaTypes.mathViewer-> + urichooser: (string list -> string list) -> unit -> script diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 454c17a7f..f5ec78ee0 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -145,14 +145,37 @@ class type console = method show : ?msg:string -> unit -> unit end -type term_source = - [ `Ast of DisambiguateTypes.term +type abouts = + [ `Blank + | `Current_proof + | `Us + ] + +type mathViewer_entry = + [ `About of abouts (* current proof *) + | `Check of string (* term *) | `Cic of Cic.term * Cic.metasenv - | `String of string + | `Dir of string (* "directory" in cic uris namespace *) + | `Uri of string (* cic object uri *) + | `Whelp of string * string list (* query and results *) ] +let string_of_entry = function + | `About `Blank -> "about:blank" + | `About `Current_proof -> "about:proof" + | `About `Us -> "about:us" + | `Check _ -> "check:" + | `Cic (_, _) -> "term:" + | `Dir uri | `Uri uri -> uri + | `Whelp (query, _) -> sprintf "whelp:%s" query + class type mathViewer = object - method show_term: term_source -> unit + (** @param reuse if set reused last opened cic browser otherwise + * opens a new one. default is false + *) + method show_entry: ?reuse:bool -> mathViewer_entry -> unit + method show_uri_list: + ?reuse:bool -> entry:mathViewer_entry -> string list -> unit end diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma index 4d7b03ce2..6e5f59010 100644 --- a/helm/matita/tests/test4.ma +++ b/helm/matita/tests/test4.ma @@ -1,4 +1,21 @@ +%% commento segato dal lexer + +(* commento che va nell'ast, ma non viene contato + come step perche' non e' un executable +*) + alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "leibnitz's equality". theorem a:0=0. -reflexivity. \ No newline at end of file + +%% commento segato dal lexer +(* nota *) + +%% questo lo si vuole tenere anche dopo la hint +hint. + +(* commenti che non devono essere colorati perche' + non c'e' nulla di eseguibile dopo di loro +*) + +%% EOF diff --git a/helm/matita/tests/test_instance.ma b/helm/matita/tests/test_instance.ma index cb3aa3fb2..82432b7c6 100644 --- a/helm/matita/tests/test_instance.ma +++ b/helm/matita/tests/test_instance.ma @@ -1,4 +1,16 @@ -instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x. -instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x. -instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z. -instance \lambda A:Set.\lambda f:A \to A \to A. \forall x,y:A. f x y = f y x. \ No newline at end of file +whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x. +whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x. +whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z. +whelp instance \lambda A:Set.\lambda f:A \to A \to A. \forall x,y:A. f x y = f y x. +whelp instance \lambda A:Set.\lambda r : A \to A \to Prop. \forall x,y,z:A. r x y \to r y z \to r x z. + + +λA:Set.λR:A\to A\to Prop.∀x:A.∀y:A.(R x y)\to ∀z:A.(R x z)\to ∃u:A.(R y u)∧(R z u) + +\lambda A:Set. \lambda R:A\to A\to Prop.\forall x:A. \forall y:A.(R x y)\to \forall z:A.(R x z)\to \exists u:A.(R y u) \land (R z u) + +\lambda A:Set. \lambda R:A\to A\to Prop. confluence A R. + +\lambda A:Set. \lambda f:A\to A\to A. \lambda g:A\to A\to A. \forall x,y,z : A . f x (g y z) = g (f x y ) (f x z). + + -- 2.39.2