From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- ide/command_windows.ml | 50 ++-- ide/command_windows.mli | 6 +- ide/coq.ml | 511 +++++++++++++++++++++++---------- ide/coq.mli | 56 +++- ide/coq.png | Bin 9101 -> 5821 bytes ide/coq_commands.ml | 11 +- ide/coqide.ml | 695 +++++++++++++++++++++++++++++---------------- ide/highlight.mll | 141 +++++---- ide/ideutils.ml | 121 +++++--- ide/ideutils.mli | 8 +- ide/index_urls.txt | 563 ------------------------------------ ide/preferences.ml | 121 +++++--- ide/preferences.mli | 11 +- ide/utf8.v | 56 ---- ide/utils/config_file.ml | 4 +- ide/utils/configwin_ihm.ml | 12 +- ide/utils/uoptions.ml | 32 +-- 17 files changed, 1170 insertions(+), 1228 deletions(-) delete mode 100644 ide/index_urls.txt delete mode 100644 ide/utf8.v (limited to 'ide') diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 937098b7..b84b0943 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -6,28 +6,30 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command_windows.ml 10197 2007-10-08 13:52:35Z notin $ *) +(* $Id: command_windows.ml 11042 2008-06-03 12:45:38Z jnarboux $ *) class command_window () = - let window = GWindow.window +(* let window = GWindow.window ~allow_grow:true ~allow_shrink:true - ~width:320 ~height:200 + ~width:500 ~height:250 ~position:`CENTER ~title:"CoqIde queries" ~show:false () - in + in *) + let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in + let _ = frame#misc#hide () in let _ = GtkData.AccelGroup.create () in - let vbox = GPack.vbox ~homogeneous:false ~packing:window#add () in + let hbox = GPack.hbox ~homogeneous:false ~packing:frame#add () in let toolbar = GButton.toolbar - ~orientation:`HORIZONTAL + ~orientation:`VERTICAL ~style:`ICONS ~tooltips:true - ~packing:(vbox#pack + ~packing:(hbox#pack ~expand:false ~fill:false) () in let notebook = GPack.notebook ~scrollable:true - ~packing:(vbox#pack + ~packing:(hbox#pack ~expand:true ~fill:true ) @@ -35,39 +37,35 @@ class command_window () = in let _ = toolbar#insert_button - ~tooltip:"Hide Window" - ~text:"Hide Window" - ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `CLOSE) - ~callback:window#misc#hide + ~tooltip:"Hide Commands Pane" + ~text:"Hide Pane" + ~icon:(Ideutils.stock_to_widget `CLOSE) + ~callback:frame#misc#hide () in let new_page_menu = toolbar#insert_button ~tooltip:"New Page" ~text:"New Page" - ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `NEW) -(* - ~callback:window#misc#hide -*) + ~icon:(Ideutils.stock_to_widget `NEW) () in let _ = toolbar#insert_button - ~tooltip:"Kill Page" - ~text:"Kill Page" - ~icon:(Ideutils.stock_to_widget ~size:`LARGE_TOOLBAR `DELETE) + ~tooltip:"Delete Page" + ~text:"Delete Page" + ~icon:(Ideutils.stock_to_widget `DELETE) ~callback:(fun () -> notebook#remove_page notebook#current_page) () in object(self) - val window = window -(* - val menubar = menubar -*) + val frame = frame + + val new_page_menu = new_page_menu val notebook = notebook - method window = window + method frame = frame method new_command ?command ?term () = let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame @@ -136,11 +134,11 @@ object(self) entry#misc#grab_default (); ignore (entry#connect#activate ~callback); ignore (combo#entry#connect#activate ~callback); - self#window#present () + self#frame#misc#show () initializer ignore (new_page_menu#connect#clicked self#new_command); - ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true)); + (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*) end let command_window = ref None diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 3a5f0d60..212e5692 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -6,16 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command_windows.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id: command_windows.mli 11011 2008-05-28 16:22:11Z jnarboux $ i*) class command_window : unit -> object method new_command : ?command:string -> ?term:string -> unit -> unit - method window : GWindow.window + method frame : GBin.frame end -val main : unit -> unit + val main : unit -> unit val command_window : unit -> command_window diff --git a/ide/coq.ml b/ide/coq.ml index d318e339..5166fb21 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 10174 2007-10-04 13:52:23Z vsiles $ *) +(* $Id: coq.ml 11126 2008-06-13 18:45:04Z herbelin $ *) open Vernac open Vernacexpr @@ -43,33 +43,38 @@ let init () = Problem: should not hide "xx is assumed" messages *) (**) - Options.make_silent true; + Flags.make_silent true; (**) Coqtop.init_ide () let i = ref 0 -let version () = +let get_version_date () = let date = if Glib.Utf8.validate Coq_config.date then Coq_config.date else "" in - let get_version_date () = - try - let ch = open_in (Coq_config.coqtop^"/revision") in - let ver = input_line ch in - let rev = input_line ch in - (ver,rev) - with _ -> (Coq_config.version,date) in - let (rev,ver) = get_version_date () in + try + let ch = open_in (Coq_config.coqtop^"/revision") in + let ver = input_line ch in + let rev = input_line ch in + (ver,rev) + with _ -> (Coq_config.version,date) + +let short_version () = + let (ver,date) = get_version_date () in + Printf.sprintf "The Coq Proof Assistant, version %s (%s)\n" ver date + +let version () = + let (ver,date) = get_version_date () in Printf.sprintf "The Coq Proof Assistant, version %s (%s)\ \nArchitecture %s running %s operating system\ \nGtk version is %s\ \nThis is the %s version (%s is the best one for this architecture and OS)\ \n" - rev ver + ver date Coq_config.arch Sys.os_type (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z) (if Mltop.get () = Mltop.Native then "native" else "bytecode") @@ -110,7 +115,310 @@ let is_in_proof_mode () = let user_error_loc l s = raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) -let interp verbosely s = +type printing_state = { + mutable printing_implicit : bool; + mutable printing_coercions : bool; + mutable printing_raw_matching : bool; + mutable printing_no_notation : bool; + mutable printing_all : bool; + mutable printing_evar_instances : bool; + mutable printing_universes : bool; + mutable printing_full_all : bool +} + +let printing_state = { + printing_implicit = false; + printing_coercions = false; + printing_raw_matching = false; + printing_no_notation = false; + printing_all = false; + printing_evar_instances = false; + printing_universes = false; + printing_full_all = false; +} + +let printing_implicit_data = ["Printing";"Implicit"], false +let printing_coercions_data = ["Printing";"Coercions"], false +let printing_raw_matching_data = ["Printing";"Matching"], true +let printing_no_synth_data = ["Printing";"Synth"], true +let printing_no_notation_data = ["Printing";"Notations"], true +let printing_all_data = ["Printing";"All"], false +let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false +let printing_universes_data = ["Printing";"Universes"], false + +let known_options = ref [] + +let prepare_option (l,dft) = + known_options := l :: !known_options; + let set = (String.concat " " ("Set"::l)) ^ "." in + let unset = (String.concat " " ("Unset"::l)) ^ "." in + if dft then unset,set else set,unset + +let coqide_known_option = function + | Goptions.TertiaryTable (a,b,c) -> List.mem [a;b;c] !known_options + | Goptions.SecondaryTable (a,b) -> List.mem [a;b] !known_options + | Goptions.PrimaryTable a -> List.mem [a] !known_options + +let with_printing_implicit = prepare_option printing_implicit_data +let with_printing_coercions = prepare_option printing_coercions_data +let with_printing_raw_matching = prepare_option printing_raw_matching_data +let with_printing_no_synth = prepare_option printing_no_synth_data +let with_printing_no_notation = prepare_option printing_no_notation_data +let with_printing_all = prepare_option printing_all_data +let with_printing_evar_instances = prepare_option printing_evar_instances_data +let with_printing_universes = prepare_option printing_universes_data + +let make_option_commands () = + let p = printing_state in + (if p.printing_implicit then [with_printing_implicit] else [])@ + (if p.printing_coercions then [with_printing_coercions] else [])@ + (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@ + (if p.printing_no_notation then [with_printing_no_notation] else [])@ + (if p.printing_all then [with_printing_all] else [])@ + (if p.printing_evar_instances then [with_printing_evar_instances] else [])@ + (if p.printing_universes then [with_printing_universes] else [])@ + (if p.printing_full_all then [with_printing_all;with_printing_evar_instances;with_printing_universes] else []) + +let make_option_commands () = + let l = make_option_commands () in + List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l; + l + +type command_attribute = + NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand + | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand + | ProofEndingCommand + +let rec attribute_of_vernac_command = function + (* Control *) + | VernacTime com -> attribute_of_vernac_command com + | VernacList _ -> [] (* unsupported *) + | VernacLoad _ -> [] + + (* Syntax *) + | VernacTacticNotation _ -> [] + | VernacSyntaxExtension _ -> [] + | VernacDelimiters _ -> [] + | VernacBindScope _ -> [] + | VernacOpenCloseScope _ -> [] + | VernacArgumentsScope _ -> [] + | VernacInfix _ -> [] + | VernacNotation _ -> [] + + (* Gallina *) + | VernacDefinition (_,_,DefineBody _,_) -> [] + | VernacDefinition (_,_,ProveBody _,_) -> [GoalStartingCommand] + | VernacStartTheoremProof _ -> [GoalStartingCommand] + | VernacEndProof _ -> [ProofEndingCommand] + | VernacExactProof _ -> [ProofEndingCommand] + + | VernacAssumption _ -> [] + | VernacInductive _ -> [] + | VernacFixpoint _ -> [] + | VernacCoFixpoint _ -> [] + | VernacScheme _ -> [] + | VernacCombinedScheme _ -> [] + + (* Modules *) + | VernacDeclareModule _ -> [] + | VernacDefineModule _ -> [] + | VernacDeclareModuleType _ -> [] + | VernacInclude _ -> [] + + (* Gallina extensions *) + | VernacBeginSection _ -> [] + | VernacEndSegment _ -> [] + | VernacRecord _ -> [] + | VernacRequire _ -> [] + | VernacImport _ -> [] + | VernacCanonical _ -> [] + | VernacCoercion _ -> [] + | VernacIdentityCoercion _ -> [] + + (* Type classes *) + | VernacClass _ -> [] + | VernacInstance _ -> [] + | VernacContext _ -> [] + | VernacDeclareInstance _ -> [] + + (* Solving *) + | VernacSolve _ -> [SolveCommand] + | VernacSolveExistential _ -> [SolveCommand] + + (* MMode *) + | VernacDeclProof -> [] + | VernacReturn -> [] + | VernacProofInstr _ -> [] + + (* Auxiliary file and library management *) + | VernacRequireFrom _ -> [] + | VernacAddLoadPath _ -> [] + | VernacRemoveLoadPath _ -> [] + | VernacAddMLPath _ -> [] + | VernacDeclareMLModule _ -> [] + | VernacChdir _ -> [OtherStatePreservingCommand] + + (* State management *) + | VernacWriteState _ -> [] + | VernacRestoreState _ -> [] + + (* Resetting *) + | VernacRemoveName _ -> [NavigationCommand] + | VernacResetName _ -> [NavigationCommand] + | VernacResetInitial -> [NavigationCommand] + | VernacBack _ -> [NavigationCommand] + | VernacBackTo _ -> [NavigationCommand] + + (* Commands *) + | VernacDeclareTacticDefinition _ -> [] + | VernacHints _ -> [] + | VernacSyntacticDefinition _ -> [] + | VernacDeclareImplicits _ -> [] + | VernacReserve _ -> [] + | VernacSetOpacity _ -> [] + | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> + [DebugCommand] + | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> + if coqide_known_option o then [KnownOptionCommand] else [] + | VernacSetOption _ -> [] + | VernacRemoveOption _ -> [] + | VernacAddOption _ -> [] + | VernacMemOption _ -> [QueryCommand] + + | VernacPrintOption _ -> [QueryCommand] + | VernacCheckMayEval _ -> [QueryCommand] + | VernacGlobalCheck _ -> [QueryCommand] + | VernacPrint _ -> [QueryCommand] + | VernacSearch _ -> [QueryCommand] + | VernacLocate _ -> [QueryCommand] + + | VernacComments _ -> [OtherStatePreservingCommand] + | VernacNop -> [OtherStatePreservingCommand] + + (* Proof management *) + | VernacGoal _ -> [GoalStartingCommand] + + | VernacAbort _ -> [NavigationCommand] + | VernacAbortAll -> [NavigationCommand] + | VernacRestart -> [NavigationCommand] + | VernacSuspend -> [NavigationCommand] + | VernacResume _ -> [NavigationCommand] + | VernacUndo _ -> [NavigationCommand] + | VernacUndoTo _ -> [NavigationCommand] + | VernacBacktrack _ -> [NavigationCommand] + + | VernacFocus _ -> [SolveCommand] + | VernacUnfocus -> [SolveCommand] + | VernacGo _ -> [] + | VernacShow _ -> [OtherStatePreservingCommand] + | VernacCheckGuard -> [OtherStatePreservingCommand] + | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand] + | VernacProof _ -> [] + + (* Toplevel control *) + | VernacToplevelControl _ -> [] + + (* Extensions *) + | VernacExtend ("Subtac_Obligations", _) -> [GoalStartingCommand] + | VernacExtend _ -> [] + +let is_vernac_goal_starting_command com = + List.mem GoalStartingCommand (attribute_of_vernac_command com) + +let is_vernac_navigation_command com = + List.mem NavigationCommand (attribute_of_vernac_command com) + +let is_vernac_query_command com = + List.mem QueryCommand (attribute_of_vernac_command com) + +let is_vernac_known_option_command com = + List.mem KnownOptionCommand (attribute_of_vernac_command com) + +let is_vernac_debug_command com = + List.mem DebugCommand (attribute_of_vernac_command com) + +let is_vernac_goal_printing_command com = + let attribute = attribute_of_vernac_command com in + List.mem GoalStartingCommand attribute or + List.mem SolveCommand attribute + +let is_vernac_state_preserving_command com = + let attribute = attribute_of_vernac_command com in + List.mem OtherStatePreservingCommand attribute or + List.mem QueryCommand attribute + +let is_vernac_tactic_command com = + List.mem SolveCommand (attribute_of_vernac_command com) + +let is_vernac_proof_ending_command com = + List.mem ProofEndingCommand (attribute_of_vernac_command com) + +type undo_info = identifier list + +let undo_info () = Pfedit.get_all_proof_names () + +type reset_mark = + | ResetToId of Names.identifier (* Relying on identifiers only *) + | ResetToState of Libnames.object_name (* Relying on states if any *) + +type reset_status = + | NoReset + | ResetAtSegmentStart of Names.identifier + | ResetAtRegisteredObject of reset_mark + +type reset_info = reset_status * undo_info * bool ref + + +let reset_mark id = match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetToState sp + | None -> ResetToId id + +let compute_reset_info = function + | VernacBeginSection id + | VernacDefineModule (_,id, _, _, _) + | VernacDeclareModule (_,id, _, _) + | VernacDeclareModuleType (id, _, _) -> + ResetAtSegmentStart (snd id), undo_info(), ref true + + | VernacDefinition (_, (_,id), DefineBody _, _) + | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) + | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> + ResetAtRegisteredObject (reset_mark id), undo_info(), ref true + + | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true + | VernacEndSegment _ -> NoReset, undo_info(), ref true + + | com when is_vernac_tactic_command com -> NoReset, undo_info(), ref true + | _ -> + (match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetAtRegisteredObject (ResetToState sp) + | None -> NoReset), undo_info(), ref true + +let reset_initial () = + prerr_endline "Reset initial called"; flush stderr; + Vernacentries.abort_refine Lib.reset_initial () + +let reset_to = function + | ResetToId id -> + prerr_endline ("Reset called with "^(string_of_id id)); + Lib.reset_name (Util.dummy_loc,id) + | ResetToState sp -> + prerr_endline + ("Reset called with state "^(Libnames.string_of_path (fst sp))); + Lib.reset_to_state sp + +let reset_to_mod id = + prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); + Lib.reset_mod (Util.dummy_loc,id) + +let raw_interp s = + Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)) + +let interp_with_options verbosely options s = prerr_endline "Starting interp..."; prerr_endline s; let pa = Pcoq.Gram.parsable (Stream.of_string s) in @@ -118,48 +426,28 @@ let interp verbosely s = match pe with | None -> assert false | Some((loc,vernac) as last) -> - match vernac with - | VernacDefinition _ | VernacStartTheoremProof _ - | VernacBeginSection _ | VernacGoal _ - | VernacDefineModule _ | VernacDeclareModuleType _ - | VernacDeclareTacticDefinition _ - when is_in_proof_mode () -> - user_error_loc loc (str "CoqIDE do not support nested goals") - | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> - user_error_loc loc (str "Debug mode not available within CoqIDE") - | VernacResetName _ - | VernacResetInitial - | VernacBack _ - | VernacAbort _ - | VernacAbortAll - | VernacRestart - | VernacSuspend - | VernacResume _ - | VernacUndo _ -> - user_error_loc loc (str "Use CoqIDE navigation instead") - | _ -> - begin - match vernac with - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - -> !flash_info - "Warning: query commands should not be inserted in scripts" - | VernacDefinition (_,_,DefineBody _,_) - | VernacInductive _ - | VernacFixpoint _ - | VernacCoFixpoint _ - | VernacEndProof _ - | VernacScheme _ - -> Options.make_silent (not verbosely) - | _ -> () - end; - Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); - Options.make_silent true; - prerr_endline ("...Done with interp of : "^s); - last + if is_vernac_debug_command vernac then + user_error_loc loc (str "Debug mode not available within CoqIDE"); + if is_vernac_navigation_command vernac then + user_error_loc loc (str "Use CoqIDE navigation instead"); + if is_vernac_known_option_command vernac then + user_error_loc loc (str "Use CoqIDE display menu instead"); + if is_vernac_query_command vernac then + !flash_info + "Warning: query commands should not be inserted in scripts"; + if not (is_vernac_goal_printing_command vernac) then + (* Verbose if in small step forward and not a tactic *) + Flags.make_silent (not verbosely); + let reset_info = compute_reset_info vernac in + List.iter (fun (set_option,_) -> raw_interp set_option) options; + raw_interp s; + Flags.make_silent true; + List.iter (fun (_,unset_option) -> raw_interp unset_option) options; + prerr_endline ("...Done with interp of : "^s); + reset_info,last + +let interp verbosely phrase = + interp_with_options verbosely (make_option_commands ()) phrase let interp_and_replace s = let result = interp false s in @@ -196,11 +484,6 @@ let try_interptac s = | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed | e -> Failed -let is_tactic = function - | VernacSolve _ -> true - | _ -> false - - let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e @@ -238,7 +521,8 @@ let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc) let interp_last last = prerr_string "*"; try - vernac_com (States.with_heavy_rollback Vernacentries.interp) last + vernac_com (States.with_heavy_rollback Vernacentries.interp) last; + Lib.add_frozen_state() with e -> let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s); raise e @@ -265,29 +549,25 @@ let prepare_hyps sigma env = in List.rev hyps -let prepare_goal sigma g = +let prepare_goal_main sigma g = let env = evar_env g in (prepare_hyps sigma env, (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl))) -let prepare_meta sigma env (m,typ) = - env, sigma, - (msg (str " ?" ++ int m ++ str " : " ++ pr_ltype_env_at_top env typ)) - -let prepare_metas info sigma env = - List.fold_right - (fun cpl acc -> - let meta = prepare_meta sigma env cpl in meta :: acc) - info.pm_subgoals [] +let prepare_goal sigma g = + let options = make_option_commands () in + List.iter (fun (set_option,_) -> raw_interp set_option) options; + let x = prepare_goal_main sigma g in + List.iter (fun (_,unset_option) -> raw_interp unset_option) options; + x let get_current_pm_goal () = let pfts = get_pftreestate () in let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in - let info = Decl_mode.get_info gls.it in - let env = pf_env gls in let sigma= sig_sig gls in - (prepare_hyps sigma env, - prepare_metas info sigma env) + let gl = sig_it gls in + prepare_goal sigma gl + let get_current_goals () = let pfts = get_pftreestate () in @@ -306,75 +586,6 @@ let print_no_goal () = msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls) -type word_class = Normal | Kwd | Reserved - - -let kwd = [(* "Compile";"Inductive";"Qed";"Type";"end";"Axiom"; - "Definition";"Load";"Quit";"Variable";"in";"Cases";"FixPoint"; - "Parameter";"Set";"of";"CoFixpoint";"Grammar";"Proof";"Syntax"; - "using";"CoInductive";"Hypothesis";"Prop";"Theorem"; - *) - "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint"; - "CoInductive"; "Defined"; "Definition"; - "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint"; - "Hypothesis"; "Immediate"; "Implicits"; "Import"; "Inductive"; - "Infix"; "Lemma"; "Load"; "Local"; - "Match"; "Module"; "Module Type"; - "Mutual"; "Parameter"; "Print"; "Proof"; "Qed"; - "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; - "Section"; "Show"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Unset"; "Variable"; "Variables"; -] - -let reserved = [] - -module SHashtbl = - Hashtbl.Make - (struct - type t = string - let equal = ( = ) - let hash = Hashtbl.hash - end) - - -let word_tbl = SHashtbl.create 37 -let _ = - List.iter (fun w -> SHashtbl.add word_tbl w Kwd) kwd; - List.iter (fun w -> SHashtbl.add word_tbl w Reserved) reserved - -let word_class s = - try - SHashtbl.find word_tbl s - with Not_found -> Normal - -type reset_info = NoReset | Reset of Names.identifier * bool ref - -let compute_reset_info = function - | VernacDefinition (_, (_,id), DefineBody _, _) - | VernacBeginSection (_,id) - | VernacDefineModule (_,(_,id), _, _, _) - | VernacDeclareModule (_,(_,id), _, _) - | VernacDeclareModuleType ((_,id), _, _) - | VernacAssumption (_, (_,((_,id)::_,_))::_) - | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> - Reset (id, ref true) - | VernacDefinition (_, (_,id), ProveBody _, _) - | VernacStartTheoremProof (_, (_,id), _, _, _) -> - Reset (id, ref false) - | _ -> NoReset - -let reset_initial () = - prerr_endline "Reset initial called"; flush stderr; - Vernacentries.abort_refine Lib.reset_initial () - -let reset_to id = - prerr_endline ("Reset called with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id) -let reset_to_mod id = - prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); - Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) - - let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = [("clear "^ident),("clear "^ident^"."); @@ -480,21 +691,9 @@ let make_cases s = [] | _ -> raise Not_found -let is_state_preserving = function - | VernacPrint _ | VernacPrintOption _ | VernacGlobalCheck _ - | VernacCheckMayEval _ | VernacSearch _ | VernacLocate _ - | VernacShow _ | VernacMemOption _ | VernacComments _ - | VernacChdir None | VernacNop -> - prerr_endline "state preserving command found"; true - | _ -> - false - - let current_status () = let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in try path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ())) with _ -> path - - diff --git a/ide/coq.mli b/ide/coq.mli index 4b4c3267..a1bea931 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -6,22 +6,59 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq.mli 9154 2006-09-20 17:18:18Z corbinea $ i*) +(*i $Id: coq.mli 11126 2008-06-13 18:45:04Z herbelin $ i*) open Names open Term open Environ open Evd +val short_version : unit -> string val version : unit -> string +type printing_state = { + mutable printing_implicit : bool; + mutable printing_coercions : bool; + mutable printing_raw_matching : bool; + mutable printing_no_notation : bool; + mutable printing_all : bool; + mutable printing_evar_instances : bool; + mutable printing_universes : bool; + mutable printing_full_all : bool +} + +val printing_state : printing_state + +type reset_mark = + | ResetToId of Names.identifier + | ResetToState of Libnames.object_name + +type reset_status = + | NoReset + | ResetAtSegmentStart of Names.identifier + | ResetAtRegisteredObject of reset_mark + +type undo_info = identifier list + +val undo_info : unit -> undo_info + +type reset_info = reset_status * undo_info * bool ref + +val compute_reset_info : Vernacexpr.vernac_expr -> reset_info +val reset_initial : unit -> unit +val reset_to : reset_mark -> unit +val reset_to_mod : identifier -> unit + val init : unit -> string list -val interp : bool -> string -> Util.loc * Vernacexpr.vernac_expr +val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr) val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit -val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string +val interp_and_replace : string -> + (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string -val is_tactic : Vernacexpr.vernac_expr -> bool -val is_state_preserving : Vernacexpr.vernac_expr -> bool +val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool +val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool +val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool +val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool (* type hyp = (identifier * constr option * constr) * string *) @@ -33,7 +70,7 @@ type goal = hyp list * concl val get_current_goals : unit -> goal list -val get_current_pm_goal : unit -> hyp list * meta list +val get_current_pm_goal : unit -> goal val get_current_goals_nb : unit -> int @@ -41,13 +78,6 @@ val print_no_goal : unit -> string val process_exn : exn -> string*(Util.loc option) -type reset_info = NoReset | Reset of Names.identifier * bool ref - -val compute_reset_info : Vernacexpr.vernac_expr -> reset_info -val reset_initial : unit -> unit -val reset_to : identifier -> unit -val reset_to_mod : identifier -> unit - val hyp_menu : hyp -> (string * string) list val concl_menu : concl -> (string * string) list diff --git a/ide/coq.png b/ide/coq.png index 2e5bdcd6..6ad66dbd 100644 Binary files a/ide/coq.png and b/ide/coq.png differ diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 677c5eff..3a48fc7d 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_commands.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: coq_commands.ml 10994 2008-05-26 16:21:31Z jnarboux $ *) let commands = [ [(* "Abort"; *) @@ -109,9 +109,9 @@ let commands = [ "Set Extraction Optimize"; "Set Hyps__limit"; "Set Implicit Arguments"; - "Set Printing Coercion"; + (*"Set Printing Coercion"; "Set Printing Coercions"; - "Set Printing Synth"; + "Set Printing Synth";*) "Set Printing Wildcard"; "Set Silent."; "Set Undo"; @@ -142,9 +142,10 @@ let commands = [ "Unset Extraction Optimize"; "Unset Hyps__limit"; "Unset Implicit Arguments"; + (* "Unset Printing Coercion"; "Unset Printing Coercions"; - "Unset Printing Synth"; + "Unset Printing Synth"; *) "Unset Printing Wildcard"; "Unset Silent."; "Unset Undo";]; @@ -156,6 +157,8 @@ let commands = [ let state_preserving = [ "Check"; "Eval"; + "Eval lazy in"; + "Eval vm_compute in"; "Eval compute in"; "Extraction"; "Extraction Library"; diff --git a/ide/coqide.ml b/ide/coqide.ml index 6cee46a6..12716197 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1,3 +1,4 @@ + (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* failwith "Internal error in out_some" | Some f -> f - let cb_ = ref None -let cb () = ((out_some !cb_):GData.clipboard) +let cb () = ((Option.get !cb_):GData.clipboard) let last_cb_content = ref "" - + let (message_view:GText.view option ref) = ref None let (proof_view:GText.view option ref) = ref None let (_notebook:GPack.notebook option ref) = ref None -let notebook () = out_some !_notebook +let notebook () = Option.get !_notebook + +let update_notebook_pos () = + let pos = + match !current.vertical_tabs, !current.opposite_tabs with + | false, false -> `TOP + | false, true -> `BOTTOM + | true , false -> `LEFT + | true , true -> `RIGHT + in + (notebook ())#set_tab_pos pos (* Tabs contain the name of the edited file and 2 status informations: Saved state + Focused proof buffer *) @@ -89,7 +97,7 @@ module Vector = struct type 'a t = ('a option) array ref let create () = ref [||] let length t = Array.length !t - let get t i = out_some (Array.get !t i) + let get t i = Option.get (Array.get !t i) let set t i v = Array.set !t i (Some v) let remove t i = Array.set !t i None let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1 @@ -101,7 +109,7 @@ module Vector = struct let exists f t = let l = Array.length !t in let rec test i = - (i < l) && (((!t.(i) <> None) && f (out_some !t.(i))) || test (i+1)) + (i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1)) in test 0 end @@ -175,7 +183,8 @@ object('self) method reset_initial : unit method send_to_coq : bool -> bool -> string -> - bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option + bool -> bool -> bool -> + (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option method set_message : string -> unit method show_pm_goal : unit method show_goals : unit @@ -300,7 +309,7 @@ let get_input_view i = let active_view = ref None -let get_active_view () = Vector.get input_views (out_some !active_view) +let get_active_view () = Vector.get input_views (Option.get !active_view) let set_active_view i = (match !active_view with None -> () | Some i -> @@ -451,8 +460,8 @@ let rec complete input_buffer w (offset:int) = end let get_current_word () = - let av = out_some ((get_current_view ()).analyzed_view) in - match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with + let av = Option.get ((get_current_view ()).analyzed_view) in + match (cb ())#text with | None -> prerr_endline "None selected"; let it = av#get_insert in @@ -481,7 +490,7 @@ let with_file name ~f = type info = {start:GText.mark; stop:GText.mark; ast:Util.loc * Vernacexpr.vernac_expr; - reset_info:Coq.reset_info; + reset_info:Coq.reset_info } exception Size of int @@ -491,60 +500,118 @@ let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0) let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0) let is_empty () = Stack.is_empty processed_stack - (* push a new Coq phrase *) -let update_on_end_of_proof id = - let lookup_lemma = function - | { ast = _, ( VernacDefinition (_, _, ProveBody _, _) - | VernacDeclareTacticDefinition _ - | VernacStartTheoremProof _) ; - reset_info = Reset (_, r) } -> - if not !r then begin - prerr_endline "Toggling Reset info to true"; - r := true; raise Exit end - else begin - prerr_endline "Toggling Changing Reset id"; - r := false - end - | { ast = _, (VernacAbort _ | VernacAbortAll | VernacGoal _) } -> raise Exit - | _ -> () - in - try Stack.iter lookup_lemma processed_stack with Exit -> () - let update_on_end_of_segment id = let lookup_section = function - | { ast = _, ( VernacBeginSection id' - | VernacDefineModule (_,id',_,_,None) - | VernacDeclareModule (_,id',_,_) - | VernacDeclareModuleType (id',_,None)); - reset_info = Reset (_, r) } - when id = id' -> raise Exit - | { reset_info = Reset (_, r) } -> r := false - | _ -> () + | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit + | { reset_info = _,_,r } -> r := false in try Stack.iter lookup_section processed_stack with Exit -> () -let push_phrase start_of_phrase_mark end_of_phrase_mark ast = +let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = let x = {start = start_of_phrase_mark; stop = end_of_phrase_mark; ast = ast; - reset_info = Coq.compute_reset_info (snd ast) - } - in - push x; + reset_info = reset_info + } in + begin match snd ast with - | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () - | VernacEndSegment id -> update_on_end_of_segment id - | _ -> () + | VernacEndSegment (_,id) -> + prerr_endline "Updating on end of segment 1"; + update_on_end_of_segment id + | _ -> () + end; + push x -let repush_phrase x = - let x = { x with reset_info = Coq.compute_reset_info (snd x.ast) } in - push x; + +let repush_phrase reset_info x = + let x = { x with reset_info = reset_info } in + begin match snd x.ast with - | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () - | VernacEndSegment id -> update_on_end_of_segment id + | VernacEndSegment (_,id) -> + prerr_endline "Updating on end of segment 2"; + update_on_end_of_segment id | _ -> () + end; + push x + +type backtrack = +| BacktrackToNextActiveMark +| BacktrackToMark of reset_mark +| BacktrackToModSec of Names.identifier +| NoBacktrack + +let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x +let add_abort = function (n,a,b,0,l) -> (0,a+1,b,0,l) | (n,a,b,p,l) -> (n,a,b,p-1,l) +let add_qed q (n,a,b,p,l) = (n,a,b,p+q,l) +let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l) + +let update_proofs (n,a,b,p,cur_lems) prev_lems = + let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in + let openproofs = List.length cur_lems - ncommon in + let closedproofs = List.length prev_lems - ncommon in + let undos = (n,a,b,p,prev_lems) in + add_qed closedproofs (Util.iterate add_abort openproofs undos) + +let pop_command undos t = + let (state_info,undo_info,section_info) = t.reset_info in + let undos = + if !section_info then + let undos = update_proofs undos undo_info in + match state_info with + | _ when is_vernac_tactic_command (snd t.ast) -> + (* A tactic, active if not below a Qed *) + add_undo undos + | ResetAtRegisteredObject mark -> + add_backtrack undos (BacktrackToMark mark) + | ResetAtSegmentStart id -> + add_backtrack undos (BacktrackToModSec id) + | _ when is_vernac_state_preserving_command (snd t.ast) -> + undos + | _ -> + add_backtrack undos BacktrackToNextActiveMark + else + begin + prerr_endline "In section"; + (* An object inside a closed section *) + add_backtrack undos BacktrackToNextActiveMark + end in + ignore (pop ()); + undos + +let rec apply_backtrack l = function + | 0, BacktrackToMark mark -> reset_to mark + | 0, NoBacktrack -> () + | 0, BacktrackToModSec id -> reset_to_mod id + | p, _ -> + (* re-synchronize Coq to the current state of the stack *) + if is_empty () then + Coq.reset_initial () + else + begin + let t = top () in + let undos = (0,0,BacktrackToNextActiveMark,p,l) in + let (_,_,b,p,l) = pop_command undos t in + apply_backtrack l (p,b); + let reset_info = Coq.compute_reset_info (snd t.ast) in + interp_last t.ast; + repush_phrase reset_info t + end + +let rec apply_undos (n,a,b,p,l) = + (* Aborts *) + if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); + (try Util.repeat a Pfedit.delete_current_proof () + with e -> prerr_endline "WARNING : found a closed environment"; raise e); + (* Undos *) + if n<>0 then + (prerr_endline ("Applying "^string_of_int n^" undos"); + try Pfedit.undo n + with _ -> (* Undo stack exhausted *) + apply_backtrack l (p,BacktrackToNextActiveMark)); + (* Reset *) + apply_backtrack l (p,b) (* For electric handlers *) exception Found @@ -556,11 +623,11 @@ let activate_input i = (match !active_view with | None -> () | Some n -> - let a_v = out_some (Vector.get input_views n).analyzed_view in + let a_v = Option.get (Vector.get input_views n).analyzed_view in a_v#deactivate (); a_v#reset_initial ); - let activate_function = (out_some (Vector.get input_views i).analyzed_view)#activate in + let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in activate_function (); set_active_view i @@ -575,13 +642,13 @@ let warning msg = class analyzed_view index = let {view = input_view_} as current_all_ = get_input_view index in - let proof_view_ = out_some !proof_view in - let message_view_ = out_some !message_view in + let proof_view_ = Option.get !proof_view in + let message_view_ = Option.get !message_view in object(self) val current_all = current_all_ val input_view = current_all_.view - val proof_view = out_some !proof_view - val message_view = out_some !message_view + val proof_view = Option.get !proof_view + val message_view = Option.get !message_view val input_buffer = input_view_#buffer val proof_buffer = proof_view_#buffer val message_buffer = message_view_#buffer @@ -794,17 +861,15 @@ object(self) proof_buffer#insert (Printf.sprintf " *** Declarative Mode ***\n"); try - let (hyps,metas) = get_current_pm_goal () in + let (hyps,concl) = get_current_pm_goal () in List.iter (fun ((_,_,_,(s,_)) as _hyp) -> proof_buffer#insert (s^"\n")) hyps; proof_buffer#insert (String.make 38 '_' ^ "\n"); - List.iter - (fun (_,_,m) -> - proof_buffer#insert (m^"\n")) - metas; + let (_,_,_,s) = concl in + proof_buffer#insert ("thesis := \n "^s^"\n"); let my_mark = `NAME "end_of_conclusion" in proof_buffer#move_mark ~where:((proof_buffer#get_iter_at_mark `INSERT)) @@ -1000,7 +1065,7 @@ object(self) self#insert_message s; message_view#misc#draw None; if localize then - (match Util.option_map Util.unloc loc with + (match Option.map Util.unloc loc with | None -> () | Some (start,stop) -> let convert_pos = byte_offset_to_char_offset phrase in @@ -1140,7 +1205,7 @@ object(self) input_view#set_editable true; !pop_info (); end in - let mark_processed complete (start,stop) ast = + let mark_processed reset_info complete (start,stop) ast = let b = input_buffer in b#move_mark ~where:stop (`NAME "start_of_input"); b#apply_tag_by_name @@ -1152,7 +1217,8 @@ object(self) end; let start_of_phrase_mark = `MARK (b#create_mark start) in let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase + push_phrase + reset_info start_of_phrase_mark end_of_phrase_mark ast; if display_goals then self#show_goals; @@ -1162,14 +1228,14 @@ object(self) None -> false | Some (loc,phrase) -> (match self#send_to_coq verbosely false phrase true true true with - | Some (complete,ast) -> - sync (mark_processed complete) loc ast; true + | Some (complete,(reset_info,ast)) -> + sync (mark_processed reset_info complete) loc ast; true | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - let mark_processed complete ast = + let mark_processed reset_info complete ast = let stop = self#get_start_of_input in if stop#starts_line then input_buffer#insert ~iter:stop insertphrase @@ -1182,7 +1248,7 @@ object(self) input_buffer#place_cursor stop; let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast; + push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast; self#show_goals; (*Auto insert save on success... try (match Coq.get_current_goals () with @@ -1203,13 +1269,15 @@ object(self) `MARK (input_buffer#create_mark start) in let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast + push_phrase + reset_info start_of_phrase_mark end_of_phrase_mark ast end | None -> ()) | _ -> ()) with _ -> ()*) in match self#send_to_coq false false coqphrase show_output show_msg localize with - | Some (complete,ast) -> sync (mark_processed complete) ast; true + | Some (complete,(reset_info,ast)) -> + sync (mark_processed reset_info complete) ast; true | None -> sync (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) @@ -1268,53 +1336,30 @@ object(self) self#clear_message)(); Coq.reset_initial () - (* backtrack Coq to the phrase preceding iterator [i] *) method backtrack_to_no_lock i = prerr_endline "Backtracking_to iter starts now."; - (* re-synchronize Coq to the current state of the stack *) - let rec synchro () = - if is_empty () then - Coq.reset_initial () - else begin - let t = pop () in - begin match t.reset_info with - | Reset (id, ({contents=true} as v)) -> v:=false; - (match snd t.ast with - | VernacBeginSection _ | VernacDefineModule _ - | VernacDeclareModule _ | VernacDeclareModuleType _ - | VernacEndSegment _ - -> reset_to_mod id - | _ -> reset_to id) - | _ -> synchro () - end; - interp_last t.ast; - repush_phrase t - end - in - let add_undo t = match t with | Some n -> Some (succ n) | None -> None - in - (* pop Coq commands until we reach iterator [i] *) + (* pop Coq commands until we reach iterator [i] *) let rec pop_commands done_smthg undos = if is_empty () then done_smthg, undos else let t = top () in - if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then begin - ignore (pop ()); - let undos = if is_tactic (snd t.ast) then add_undo undos else None in - pop_commands true undos - end else - done_smthg, undos + if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then + begin + prerr_endline "Popped top command"; + pop_commands true (pop_command undos t) + end + else + done_smthg, undos in - let done_smthg, undos = pop_commands false (Some 0) in + let undos = (0,0,NoBacktrack,0,undo_info()) in + let done_smthg, undos = pop_commands false undos in prerr_endline "Popped commands"; if done_smthg then - begin - try - (match undos with - | None -> synchro () - | Some n -> try Pfedit.undo n with _ -> synchro ()); + begin + try + apply_undos undos; sync (fun _ -> let start = if is_empty () then input_buffer#start_iter @@ -1342,7 +1387,8 @@ Please restart and report NOW."; method backtrack_to i = if Mutex.try_lock coq_may_stop then - (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop; + (!push_info "Undoing..."; + self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop; !pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" @@ -1377,41 +1423,9 @@ Please restart and report NOW."; self#show_goals; self#clear_message in - begin match last_command with - | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> - begin - try Pfedit.undo 1; ignore (pop ()); sync update_input () - with _ -> self#backtrack_to_no_lock start - end - | {ast=_,t;reset_info=Reset (id, {contents=true})} -> - ignore (pop ()); - (match t with - | VernacBeginSection _ | VernacDefineModule _ - | VernacDeclareModule _ | VernacDeclareModuleType _ - | VernacEndSegment _ - -> reset_to_mod id - | _ -> reset_to id); - sync update_input () - | { ast = _, ( VernacStartTheoremProof _ - | VernacGoal _ - | VernacDeclareTacticDefinition _ - | VernacDefinition (_,_,ProveBody _,_)); - reset_info=Reset(id,{contents=false})} -> - ignore (pop ()); - (try - Pfedit.delete_current_proof () - with e -> - begin - prerr_endline "WARNING : found a closed environment"; - raise e - end); - sync update_input () - | { ast = (_, a) } when is_state_preserving a -> - ignore (pop ()); - sync update_input () - | _ -> - self#backtrack_to_no_lock start - end; + let undo = pop_command (0,0,NoBacktrack,0,undo_info()) last_command in + apply_undos undo; + sync update_input () with | Size 0 -> (* !flash_info "Nothing to Undo"*)() ); @@ -1533,7 +1547,7 @@ Please restart and report NOW."; deact_id <- Some (input_view#event#connect#key_press self#disconnected_keypress_handler); prerr_endline "CONNECTED inactive : "; - print_id (out_some deact_id) + print_id (Option.get deact_id) method activate () = is_active <- true; @@ -1545,9 +1559,9 @@ Please restart and report NOW."; act_id <- Some (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; - print_id (out_some act_id); + print_id (Option.get act_id); match - (out_some ((Vector.get input_views index).analyzed_view)) #filename + (Option.get ((Vector.get input_views index).analyzed_view)) #filename with | None -> () | Some f -> let dir = Filename.dirname f in @@ -1645,7 +1659,7 @@ Please restart and report NOW."; if auto_complete_on && String.length s = 1 && s <> " " && s <> "\n" then - let v = out_some (get_current_view ()).analyzed_view + let v = Option.get (get_current_view ()).analyzed_view in let has_completed = v#complete_at_offset @@ -1662,7 +1676,7 @@ Please restart and report NOW."; (fun () -> if input_buffer#modified then set_tab_image index - ~icon:(match (out_some (current_all.analyzed_view))#filename with + ~icon:(match (Option.get (current_all.analyzed_view))#filename with | None -> `SAVE_AS | Some _ -> `SAVE ) @@ -1899,10 +1913,19 @@ let main files = | Vector.Found i -> set_current_view i | e -> !flash_info ("Load failed: "^(Printexc.to_string e)) in - let load_m = file_factory#add_item "_Open/Create" + let load_m = file_factory#add_item "_New" + ~key:GdkKeysyms._N in + let load_f () = + match select_file_for_save ~title:"Create file" () with + | None -> () + | Some f -> load f + in + ignore (load_m#connect#activate (load_f)); + + let load_m = file_factory#add_item "_Open" ~key:GdkKeysyms._O in let load_f () = - match select_file ~title:"Load file" () with + match select_file_for_open ~title:"Load file" () with | None -> () | Some f -> load f in @@ -1916,20 +1939,20 @@ let main files = let save_f () = let current = get_current_view () in try - (match (out_some current.analyzed_view)#filename with + (match (Option.get current.analyzed_view)#filename with | None -> - begin match GToolbox.select_file ~title:"Save file" () + begin match select_file_for_save ~title:"Save file" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info ("File " ^ f ^ " saved") end else warning ("Save Failed (check if " ^ f ^ " is writable)") end | Some f -> - if (out_some current.analyzed_view)#save f then + if (Option.get current.analyzed_view)#save f then !flash_info ("File " ^ f ^ " saved") else warning ("Save Failed (check if " ^ f ^ " is writable)") @@ -1944,27 +1967,27 @@ let main files = in let saveas_f () = let current = get_current_view () in - try (match (out_some current.analyzed_view)#filename with + try (match (Option.get current.analyzed_view)#filename with | None -> - begin match GToolbox.select_file ~title:"Save file as" () + begin match select_file_for_save ~title:"Save file as" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info "Saved" end else !flash_info "Save Failed" end | Some f -> - begin match GToolbox.select_file + begin match select_file_for_save ~dir:(ref (Filename.dirname f)) ~filename:(Filename.basename f) ~title:"Save file as" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info "Saved" end else !flash_info "Save Failed" @@ -1974,7 +1997,7 @@ let main files = ignore (saveas_m#connect#activate saveas_f); (* File/Save All Menu *) - let saveall_m = file_factory#add_item "Sa_ve All" in + let saveall_m = file_factory#add_item "Sa_ve all" in let saveall_f () = Vector.iter (function @@ -1997,7 +2020,7 @@ let main files = ignore (saveall_m#connect#activate saveall_f); (* File/Revert Menu *) - let revert_m = file_factory#add_item "_Revert All Buffers" in + let revert_m = file_factory#add_item "_Revert all buffers" in let revert_f () = Vector.iter (function @@ -2018,9 +2041,9 @@ let main files = (* File/Close Menu *) let close_m = - file_factory#add_item "_Close Buffer" ~key:GdkKeysyms._W in + file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in let close_f () = - let v = out_some !active_view in + let v = Option.get !active_view in let act = get_current_view_page () in if v = act then !flash_info "Cannot close an active view" else remove_current_view_page () @@ -2030,7 +2053,7 @@ let main files = (* File/Print Menu *) let print_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot print: this buffer has no name" @@ -2040,17 +2063,48 @@ let main files = !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^ " | " ^ !current.cmd_print in - let s,_ = run_command av#insert_message cmd in - !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + let print_window = GWindow.window + ~title:"Print" + ~modal:true + ~position:`CENTER + ~wm_class:"CodIDE" + ~wm_name: "CodIDE" () in + let vbox_print = GPack.vbox + ~spacing:10 + ~border_width:10 + ~packing:print_window#add () in + let _ = GMisc.label + ~justify:`LEFT + ~text:"Print using the following command:" + ~packing:vbox_print#add () in + let print_entry = GEdit.entry + ~text:cmd + ~editable:true + ~width_chars:80 + ~packing:vbox_print#add () in + let hbox_print = GPack.hbox + ~spacing:10 + ~packing:vbox_print#add () in + let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in + let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in + let callback_print () = + let cmd = print_entry#text in + let s,_ = run_command av#insert_message cmd in + !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); + print_window#destroy () + in + ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ; + ignore (print_button#connect#clicked ~callback:callback_print); + print_window#misc#show(); in - let _ = file_factory#add_item "_Print" + let _ = file_factory#add_item "_Print..." ~key:GdkKeysyms._P ~callback:print_f in (* File/Export to Menu *) let export_f kind () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot print: this buffer has no name" @@ -2060,11 +2114,11 @@ let main files = let basef_we = try Filename.chop_extension basef with _ -> basef in match kind with | "latex" -> basef_we ^ ".tex" - | "dvi" | "ps" | "html" -> basef_we ^ "." ^ kind + | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind | _ -> assert false in let cmd = - "cd " ^ (Filename.quote (Filename.dirname f)) ^ "; " ^ + "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) in let s,_ = run_command av#insert_message cmd in @@ -2085,6 +2139,9 @@ let main files = let _ = file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") in + let _ = + file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf") + in let _ = file_export_factory#add_item "_Ps" ~callback:(export_f "ps") in @@ -2095,7 +2152,7 @@ let main files = (fun () -> Highlight.highlight_all (get_current_view()).view#buffer; - (out_some (get_current_view()).analyzed_view)#recenter_insert)); + (Option.get (get_current_view()).analyzed_view)#recenter_insert)); (* File/Quit Menu *) let quit_f () = @@ -2129,7 +2186,7 @@ let main files = ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback: (do_if_not_computing "undo" (fun () -> - ignore ((out_some ((get_current_view()).analyzed_view))# + ignore ((Option.get ((get_current_view()).analyzed_view))# without_auto_complete (fun () -> (get_current_view()).view#undo) ())))); ignore(edit_f#add_item "_Clear Undo Stack" @@ -2203,13 +2260,15 @@ let main files = ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X) () in - let _ = + (* let _ = GButton.check_button ~label:"case sensitive" ~active:true ~packing: (find_box#attach ~left:1 ~top:2) () - in + + in + *) (* let find_backwards_check = GButton.check_button @@ -2385,7 +2444,7 @@ let main files = ~callback: (do_if_not_computing (fun b -> - let v = out_some (get_current_view ()).analyzed_view + let v = Option.get (get_current_view ()).analyzed_view in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset) @@ -2397,7 +2456,7 @@ let main files = ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: (fun () -> ignore ( - let av = out_some ((get_current_view()).analyzed_view) in + let av = Option.get ((get_current_view()).analyzed_view) in av#complete_at_offset (av#get_insert)#offset ))); @@ -2406,13 +2465,13 @@ let main files = let _ = edit_f#add_item "External editor" ~callback: (fun () -> - let av = out_some ((get_current_view()).analyzed_view) in + let av = Option.get ((get_current_view()).analyzed_view) in match av#filename with | None -> () | Some f -> save_f (); - let l,r = !current.cmd_editor in - let _ = run_command av#insert_message (l ^ (Filename.quote f) ^ r) in + let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in + let _ = run_command av#insert_message com in av#revert) in let _ = edit_f#add_separator () in @@ -2454,7 +2513,7 @@ let main files = let _ = edit_f#add_item "_Preferences" - ~callback:(fun () -> configure ();reset_revert_timer ()) + ~callback:(fun () -> configure ~apply:update_notebook_pos (); reset_revert_timer ()) in (* let save_prefs_m = @@ -2472,7 +2531,7 @@ let main files = in let do_or_activate f () = let current = get_current_view () in - let analyzed_view = out_some current.analyzed_view in + let analyzed_view = Option.get current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) else @@ -2496,7 +2555,7 @@ let main files = end; ignore (toolbar#insert_button ~tooltip - ~text:tooltip +(* ~text:tooltip*) ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR icon) ~callback ()) @@ -2544,8 +2603,7 @@ let main files = ~tooltip:"Interrupt computations" ~key:GdkKeysyms._Break ~callback:break - `STOP - ; + `STOP; (* Tactics Menu *) let tactics_menu = factory#add_submenu "_Try Tactics" in @@ -2557,7 +2615,7 @@ let main files = in let do_if_active_raw f () = let current = get_current_view () in - let analyzed_view = out_some current.analyzed_view in + let analyzed_view = Option.get current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) in let do_if_active f = @@ -2628,6 +2686,8 @@ let main files = )) ()); + + ignore (tactics_factory#add_item "" ~key:GdkKeysyms._dollar ~callback:(do_if_active (fun a -> a#tactic_wizard @@ -2830,6 +2890,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~term ()) in + let _ = + queries_factory#add_item "_Locate" + ~callback:(fun () -> let term = get_current_word () in + (Command_windows.command_window ())#new_command + ~command:"Locate" + ~term + ()) + in let _ = queries_factory#add_item "_Whelp Locate" ~callback:(fun () -> let term = get_current_word () in @@ -2839,6 +2907,84 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ()) in + (* Display menu *) + + let display_menu = factory#add_submenu "_Display" in + let view_factory = new GMenu.factory display_menu + ~accel_path:"/Display/" + ~accel_group + ~accel_modi:!current.modifier_for_display + in + + let _ = ignore (view_factory#add_check_item + "Display _implicit arguments" + ~key:GdkKeysyms._i + ~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Display _coercions" + ~key:GdkKeysyms._c + ~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Display raw _matching expressions" + ~key:GdkKeysyms._m + ~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Deactivate _notations display" + ~key:GdkKeysyms._n + ~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Display _all basic low-level contents" + ~key:GdkKeysyms._a + ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Display _existential variable instances" + ~key:GdkKeysyms._e + ~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Display _universe levels" + ~key:GdkKeysyms._u + ~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in + + let _ = ignore (view_factory#add_check_item + "Display all _low-level contents" + ~key:GdkKeysyms._l + ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in + + (* Unicode *) +(* + let unicode_menu = factory#add_submenu "_Unicode" in + let unicode_factory = new GMenu.factory unicode_menu + ~accel_path:"/Unicode/" + ~accel_group + ~accel_modi:[] + in + let logic_symbols_menu = unicode_factory#add_submenu "Math operators" in + let logic_factory = new GMenu.factory logic_symbols_menu + ~accel_path:"/Unicode/Math operators" + ~accel_group + ~accel_modi:[] + in + let new_unicode_item s = ignore ( + logic_factory#add_item s + ~callback:(fun () -> + let v = get_current_view () in + ignore (v.view#buffer#insert_interactive s))) + in + + for i = 0x2200 to 0x22FF do + List.iter new_unicode_item [Glib.Utf8.from_unichar i]; + + done; + +*) + + (* Externals *) let externals_menu = factory#add_submenu "_Compile" in let externals_factory = new GMenu.factory externals_menu @@ -2850,7 +2996,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Compile Menu *) let compile_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in save_f (); match av#filename with | None -> @@ -2877,21 +3023,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Make Menu *) let make_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> - !flash_info "Cannot print: this buffer has no name" + !flash_info "Cannot make: this buffer has no name" | Some f -> let cmd = "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in - (* - save_f (); - *) - av#insert_message "Command output:\n"; - let s,res = run_command av#insert_message cmd in - last_make := res; - last_make_index := 0; - !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + + (* + save_f (); + *) + av#insert_message "Command output:\n"; + let s,res = run_command av#insert_message cmd in + last_make := res; + last_make_index := 0; + !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in let _ = externals_factory#add_item "_Make" ~key:GdkKeysyms._F6 @@ -2905,7 +3052,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let file,line,start,stop,error_msg = search_next_error () in load file; let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in let input_buffer = v.view#buffer in (* let init = input_buffer#start_iter in @@ -2931,7 +3078,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); with Not_found -> last_make_index := 0; let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in av#set_message "No more errors.\n" in let _ = @@ -2943,7 +3090,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/CoqMakefile Menu*) let coq_makefile_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot make makefile: this buffer has no name" @@ -2958,20 +3105,24 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in (* Windows Menu *) let configuration_menu = factory#add_submenu "_Windows" in - let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"/Windows" ~accel_group + let configuration_factory = new GMenu.factory configuration_menu + ~accel_path:"/Windows" + ~accel_modi:[] + ~accel_group in - let _ = + let _ = configuration_factory#add_item - "Show _Query Window" - (* - ~key:GdkKeysyms._F12 - *) - ~callback:(Command_windows.command_window ())#window#present + "Show/Hide _Query Pane" + ~key:GdkKeysyms._Escape + ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then + (Command_windows.command_window ())#frame#misc#hide () + else + (Command_windows.command_window ())#frame#misc#show ()) in let _ = - configuration_factory#add_item + configuration_factory#add_check_item "Show/Hide _Toolbar" - ~callback:(fun () -> + ~callback:(fun _ -> !current.show_toolbar <- not !current.show_toolbar; !show_toolbar !current.show_toolbar) in @@ -2983,8 +3134,15 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let nb = notebook () in if nb#misc#toplevel#get_oid=w#coerce#get_oid then begin - let nw = GWindow.window ~show:true () in - let parent = out_some nb#misc#parent in + let nw = GWindow.window + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~position:`CENTER + ~wm_name:"CoqIde" + ~wm_class:"CoqIde" + ~title:"Script" + ~show:true () in + let parent = Option.get nb#misc#parent in ignore (nw#connect#destroy ~callback: (fun () -> nb#misc#reparent parent)); @@ -2993,6 +3151,33 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); end ))) in +(* let _ = configuration_factory#add_item + "Detach _Command Pane" + ~callback: + (do_if_not_computing "detach command pane" (sync + (fun () -> + let command_object = Command_windows.command_window() in + let queries_frame = command_object#frame in + if queries_frame#misc#toplevel#get_oid=w#coerce#get_oid then + begin + let nw = GWindow.window + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~wm_name:"CoqIde" + ~wm_class:"CoqIde" + ~position:`CENTER + ~title:"Queries" + ~show:true () in + let parent = Option.get queries_frame#misc#parent in + ignore (nw#connect#destroy + ~callback: + (fun () -> queries_frame#misc#reparent parent)); + queries_frame#misc#show(); + queries_frame#misc#reparent nw#coerce + end + ))) + in +*) let _ = configuration_factory#add_item "Detach _View" @@ -3002,8 +3187,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); match get_current_view () with | {view=v;analyzed_view=Some av} -> let w = GWindow.window ~show:true - ~width:(!current.window_width/2) - ~height:(!current.window_height) + ~width:(!current.window_width*2/3) + ~height:(!current.window_height*2/3) + ~position:`CENTER ~title:(match av#filename with | None -> "*Unnamed*" | Some f -> f) @@ -3037,17 +3223,17 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let _ = help_factory#add_item "Browse Coq _Manual" ~callback: (fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in browse av#insert_message (!current.doc_url ^ "main.html")) in let _ = help_factory#add_item "Browse Coq _Library" ~callback: (fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in browse av#insert_message !current.library_url) in let _ = help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1 ~callback:(fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in av#help_for_keyword ()) in let _ = help_factory#add_separator () in @@ -3055,19 +3241,20 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let faq_m = help_factory#add_item "_FAQ" in *) let about_m = help_factory#add_item "_About" in - (* End of menu *) (* The vertical Separator between Scripts and Goals *) - let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:vbox#add () in + let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in + let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(queries_pane#pack1 ~shrink:false ~resize:true) () in let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true ~packing:fr_notebook#add ()); + update_notebook_pos (); let nb = notebook () in let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in - let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in + let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in let sw2 = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC @@ -3076,6 +3263,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(fr_b#add) () in + let command_object = Command_windows.command_window() in + let queries_frame = command_object#frame in + queries_pane#pack2 ~shrink:false ~resize:false (queries_frame#coerce); let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) () in @@ -3312,32 +3502,46 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (fun {view=view} -> view#misc#modify_font fd) input_views; ); - let about (b:GText.buffer) = - (try - let image = lib_ide_file "coq.png" in - let startup_image = GdkPixbuf.from_file image in - b#insert_pixbuf ~iter:b#start_iter - ~pixbuf:startup_image; - b#insert ~iter:b#start_iter "\t\t"; - with _ -> ()); - let about_string = - "\nCoqIDE: an Integrated Development Environment for Coq\n\ + let about_full_string = + "\nCoq is developed by the Coq Development Team\ + \n(INRIA - CNRS - University Paris 11 and partners)\ + \nWeb site: http://coq.inria.fr\ + \nFeature wish or bug report: http://logical.saclay.inria.fr/coq-bugs\ + \n\ + \nCredits for CoqIDE, the Integrated Development Environment for Coq:\ + \n\ \nMain author : Benjamin Monate\ \nContributors : Jean-Christophe Filliâtre\ - \n Pierre Letouzey, Claude Marché\n\ - \nFeature wish or bug report: use Web interface\n\ - \n\thttp://logical.futurs.inria.fr/coq-bugs\n\ + \n Pierre Letouzey, Claude Marché\ + \n Bruno Barras, Pierre Corbineau\ + \n Julien Narboux, Hugo Herbelin, ... \ + \n\ \nVersion information\ - \n-------------------\n" - in - if Glib.Utf8.validate about_string - then b#insert about_string; - let coq_version = Coq.version () in - if Glib.Utf8.validate coq_version - then b#insert coq_version; - + \n-------------------\ + \n" + in + let initial_about (b:GText.buffer) = + (try + let image = lib_ide_file "coq.png" in + let startup_image = GdkPixbuf.from_file image in + b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; + b#insert ~iter:b#start_iter "\t\t " + with _ -> ()); + let coq_version = Coq.short_version () in + b#insert ~iter:b#start_iter "\n\n"; + if Glib.Utf8.validate coq_version then b#insert ~iter:b#start_iter coq_version; + b#insert ~iter:b#start_iter "\n " in - about tv2#buffer; + + let about (b:GText.buffer) = + if Glib.Utf8.validate about_full_string + then b#insert about_full_string; + let coq_version = Coq.version () in + if Glib.Utf8.validate coq_version + then b#insert coq_version + + in + initial_about tv2#buffer; w#add_accel_group accel_group; (* Remove default pango menu for textviews *) ignore (tv2#event#connect#button_press ~callback: @@ -3395,7 +3599,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (fun _ -> if !current.contextual_menus_on_goal then begin - let w = (out_some (get_active_view ()).analyzed_view) in + let w = (Option.get (get_active_view ()).analyzed_view) in !push_info "Computing advanced goal's menus"; prerr_endline "Entering Goal Window. Computing Menus...."; w#show_goals_full; @@ -3468,6 +3672,7 @@ let start () = else failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); Blaster_window.main 9; + init_stdout (); main files; if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); while true do @@ -3480,5 +3685,3 @@ let start () = flush stderr; crash_save 127 done - - diff --git a/ide/highlight.mll b/ide/highlight.mll index 2f099208..8cd55c97 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: highlight.mll 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: highlight.mll 11004 2008-05-28 09:09:12Z herbelin $ *) { @@ -18,18 +18,15 @@ let comment_start = ref 0 - let is_keyword = + (* Without this table, the automaton would be too big and + ocamllex would fail *) + let is_one_word_command = let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) - [ "Add" ; "Check"; "Defined" ; - "End" ; "Eval"; "Export" ; "Extraction" ; "Hint" ; "Hints" ; - "Implicits" ; "Import" ; - "Infix" ; "Load" ; "Module" ; - "Notation"; "Proof" ; "Print"; "Qed" ; - "Require" ; "Reset"; "Undo"; "Save" ; - "Section" ; "Unset" ; - "Set" ; "Notation"; - "Implicit"; "Arguments"; "Unfold"; "Resolve" + [ "Add" ; "Check"; "Eval"; "Extraction" ; + "Load" ; "Undo"; "Goal"; + "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ; + "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]; Hashtbl.mem h @@ -38,20 +35,31 @@ List.iter (fun s -> Hashtbl.add h s ()) [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; "end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return"; - "Prop"; "Set"; "Type"]; + "Prop"; "Set"; "Type" ]; Hashtbl.mem h - let is_declaration = + (* Without this table, the automaton would be too big and + ocamllex would fail *) + let is_one_word_declaration = let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) - [ "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; "Proposition" ; "Property" ; - "Definition" ; "Let" ; "Example" ; "SubClass" ; "Inductive" ; "CoInductive" ; - "Record" ; "Structure" ; "Fixpoint" ; "CoFixpoint"; + [ (* Theorems *) + "Theorem" ; "Lemma" ; "Fact" ; "Remark" ; "Corollary" ; + "Proposition" ; "Property" ; + (* Definitions *) + "Definition" ; "Let" ; "Example" ; "SubClass" ; + "Fixpoint" ; "CoFixpoint" ; "Scheme" ; + (* Assumptions *) "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; - "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters" + "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"; + (* Inductive *) + "Inductive" ; "CoInductive" ; "Record" ; "Structure" ; + (* Other *) + "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" ]; Hashtbl.mem h + let starting = ref true } let space = @@ -62,44 +70,67 @@ let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let ident = firstchar identchar* -let thm_token = "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" - -let def_token = "Definition" | "Let" | "Example" | "SubClass" - -let assumption = "Hypothesis" | "Variable" | "Axiom" | "Parameter" | "Conjecture" | - "Hypotheses" | "Variables" | "Axioms" | "Parameters" - -let declaration = - "Theorem" | "Lemma" | "Fact" | "Remark" | "Corollary" | "Proposition" | "Property" | - "Definition" | "Let" | "Example" | "SubClass" | - "Inductive" | "CoInductive" | - "Record" | "Structure" | - "Fixpoint" | "CoFixpoint" - +let multiword_declaration = + "Module" (space+ "Type")? +| "Program" space+ ident +| "Existing" space+ "Instance" +| "Canonical" space+ "Structure" + +let locality = ("Local" space+)? + +let multiword_command = + "Set" (space+ ident)* +| "Unset" (space+ ident)* +| "Open" space+ locality "Scope" +| "Close" space+ locality "Scope" +| "Bind" space+ "Scope" +| "Arguments" space+ "Scope" +| "Reserved" space+ "Notation" space+ locality +| "Delimit" space+ "Scope" +| "Next" space+ "Obligation" +| "Solve" space+ "Obligations" +| "Require" space+ ("Import"|"Export")? +| "Infix" space+ locality +| "Notation" space+ locality +| "Hint" space+ locality ident +| "Reset" (space+ "Initial")? +| "Tactic" space+ "Notation" +| "Implicit" space+ "Arguments" +| "Implicit" space+ ("Type"|"Types") +| "Combined" space+ "Scheme" + +(* At least still missing: "Inline" + decl, variants of "Identity + Coercion", variants of Print, Add, ... *) + +rule next_starting_order = parse + | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } + | space+ { next_starting_order lexbuf } + | multiword_declaration + { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "decl" } + | multiword_command + { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } + | ident as id + { starting:=false; + if is_one_word_command id then + lexeme_start lexbuf, lexeme_end lexbuf, "kwd" + else if is_one_word_declaration id then + lexeme_start lexbuf, lexeme_end lexbuf, "decl" + else + next_interior_order lexbuf + } + | _ { starting := false; next_interior_order lexbuf} + | eof { raise End_of_file } -rule next_order = parse +and next_interior_order = parse | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } - | "Module Type" - { lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } - | "Program" space+ ident as id { lexeme_start lexbuf, lexeme_end lexbuf, "decl" } | ident as id - { if is_keyword id then - lexeme_start lexbuf, lexeme_end lexbuf, "kwd" - else - begin - if is_constr_kw id then - lexeme_start lexbuf, lexeme_end lexbuf, "kwd" - else - begin - if is_declaration id then - lexeme_start lexbuf, lexeme_end lexbuf, "decl" - else - next_order lexbuf - end - end - } - | _ { next_order lexbuf} + { if is_constr_kw id then + lexeme_start lexbuf, lexeme_end lexbuf, "kwd" + else + next_interior_order lexbuf } + | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf } + | _ { next_interior_order lexbuf} | eof { raise End_of_file } and comment = parse @@ -114,6 +145,7 @@ and comment = parse let highlighting = ref false let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop = + starting := true; (* approximation: assume the beginning of a sentence *) if !highlighting then prerr_endline "Rejected highlight" else begin highlighting := true; @@ -130,7 +162,10 @@ and comment = parse let lb = Lexing.from_string s in try while true do - let b,e,o=next_order lb in + let b,e,o = + if !starting then next_starting_order lb + else next_interior_order lb in + let b,e = convert_pos b,convert_pos e in let start = input_buffer#get_iter_at_char (offset + b) in let stop = input_buffer#get_iter_at_char (offset + e) in @@ -142,7 +177,7 @@ and comment = parse highlighting := false end - let highlight_current_line input_buffer = + let highlight_current_line input_buffer = try let i = get_insert input_buffer in highlight_slice input_buffer (i#set_line_offset 0) i diff --git a/ide/ideutils.ml b/ide/ideutils.ml index df4594a7..d851dc2f 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 9263 2006-10-23 12:08:08Z barras $ *) +(* $Id: ideutils.ml 11093 2008-06-10 18:41:33Z barras $ *) open Preferences @@ -25,7 +25,7 @@ let set_location = ref (function s -> failwith "not ready") let pulse = ref (function () -> failwith "not ready") -let debug = Options.debug +let debug = Flags.debug let prerr_endline s = if !debug then (prerr_endline s;flush stderr) @@ -35,7 +35,7 @@ let prerr_string s = let lib_ide_file f = let coqlib = System.getenv_else "COQLIB" - (if Coq_config.local || !Options.boot then Coq_config.coqtop + (if Coq_config.local || !Flags.boot then Coq_config.coqtop else Coq_config.coqlib) in Filename.concat (Filename.concat coqlib "ide") f @@ -148,44 +148,83 @@ let set_highlight_timer f = (* Get back the standard coq out channels *) -let read_stdout,clear_stdout = +let init_stdout,read_stdout,clear_stdout = let out_buff = Buffer.create 100 in - Pp_control.std_ft := Format.formatter_of_buffer out_buff; - (fun () -> Format.pp_print_flush !Pp_control.std_ft (); + let out_ft = Format.formatter_of_buffer out_buff in + let deep_out_ft = Format.formatter_of_buffer out_buff in + let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in + (fun () -> + Pp_control.std_ft := out_ft; + Pp_control.err_ft := out_ft; + Pp_control.deep_ft := deep_out_ft; +), + (fun () -> Format.pp_print_flush out_ft (); let r = Buffer.contents out_buff in + prerr_endline "Output from Coq is: "; prerr_endline r; Buffer.clear out_buff; r), (fun () -> - Format.pp_print_flush !Pp_control.std_ft (); Buffer.clear out_buff) + Format.pp_print_flush out_ft (); Buffer.clear out_buff) let last_dir = ref "" -let select_file ~title ?(dir = last_dir) ?(filename="") () = - let fs = - if Filename.is_relative filename then begin - if !dir <> "" then - let filename = Filename.concat !dir filename in - GWindow.file_selection ~show_fileops:true ~modal:true ~title ~filename () - else - GWindow.file_selection ~show_fileops:true ~modal:true ~title () - end else begin - dir := Filename.dirname filename; - GWindow.file_selection ~show_fileops:true ~modal:true ~title ~filename () - end - in - fs#complete ~filter:""; - ignore (fs#connect#destroy ~callback: GMain.Main.quit); - let file = ref None in - ignore (fs#ok_button#connect#clicked ~callback: - begin fun () -> - file := Some fs#filename; - dir := Filename.dirname fs#filename; - fs#destroy () - end); - ignore (fs # cancel_button # connect#clicked ~callback:fs#destroy); - fs # show (); - GMain.Main.main (); - !file +let filter_all_files () = GFile.filter + ~name:"All" + ~patterns:["*"] () + +let filter_coq_files () = GFile.filter + ~name:"Coq source code" + ~patterns:[ "*.v"] () + +let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = + let file = ref None in + let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () in + file_chooser#add_button_stock `CANCEL `CANCEL ; + file_chooser#add_select_button_stock `OPEN `OPEN ; + file_chooser#add_filter (filter_coq_files ()); + file_chooser#add_filter (filter_all_files ()); + file_chooser#set_default_response `OPEN; + ignore (file_chooser#set_current_folder !dir); + begin match file_chooser#run () with + | `OPEN -> + begin + file := file_chooser#filename; + match !file with + None -> () + | Some s -> dir := Filename.dirname s; + end + | `DELETE_EVENT | `CANCEL -> () + end ; + file_chooser#destroy (); + !file + + +let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = + let file = ref None in + let file_chooser = GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title () in + file_chooser#add_button_stock `CANCEL `CANCEL ; + file_chooser#add_select_button_stock `SAVE `SAVE ; + file_chooser#add_filter (filter_coq_files ()); + file_chooser#add_filter (filter_all_files ()); + (* this line will be used when a lablgtk >= 2.10.0 is the default on most distributions + file_chooser#set_do_overwrite_confirmation true; + *) + file_chooser#set_default_response `SAVE; + ignore (file_chooser#set_current_folder !dir); + ignore (file_chooser#set_current_name filename); + + begin match file_chooser#run () with + | `SAVE -> + begin + file := file_chooser#filename; + match !file with + None -> () + | Some s -> dir := Filename.dirname s; + end + | `DELETE_EVENT | `CANCEL -> () + end ; + file_chooser#destroy (); + !file let find_tag_start (tag :GText.tag) (it:GText.iter) = let it = it#copy in @@ -252,10 +291,8 @@ let run_command f c = let buffe = String.make 127 ' ' in let n = ref 0 in let ne = ref 0 in - - while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; - !n+ !ne <> 0 - do + while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0 + do let r = try_convert (String.sub buff 0 !n) in f r; Buffer.add_string result r; @@ -266,9 +303,11 @@ let run_command f c = (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) let browse f url = - let l,r = !current.cmd_browse in - let (_s,_res) = run_command f (l ^ url ^ r) in - () + let com = Flags.subst_command_placeholder !current.cmd_browse url in + let s = Sys.command com in + if s = 127 then + f ("Could not execute\n\""^com^ + "\"\ncheck your preferences for setting a valid browser command\n") let url_for_keyword = let ht = Hashtbl.create 97 in @@ -293,7 +332,7 @@ let url_for_keyword = let browse_keyword f text = try let u = url_for_keyword text in browse f (!current.doc_url ^ u) - with _ -> () + with Not_found -> f ("No documentation found for "^text) let underscore = Glib.Utf8.to_unichar "_" (ref 0) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 3af80f47..48ff0fca 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ideutils.mli 7608 2005-11-25 17:09:25Z barras $ i*) +(*i $Id: ideutils.mli 11006 2008-05-28 10:42:45Z jnarboux $ i*) val async : ('a -> unit) -> 'a -> unit val sync : ('a -> 'b) -> 'a -> 'b @@ -17,6 +17,7 @@ val mutex : string -> ('a -> unit) -> 'a -> unit val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int +val init_stdout : unit -> unit val clear_stdout : unit -> unit val debug : bool ref val disconnect_revert_timer : unit -> unit @@ -39,7 +40,10 @@ val print_id : 'a -> unit val read_stdout : unit -> string val revert_timer : GMain.Timeout.id option ref val auto_save_timer : GMain.Timeout.id option ref -val select_file : +val select_file_for_open : + title:string -> + ?dir:string ref -> ?filename:string -> unit -> string option +val select_file_for_save : title:string -> ?dir:string ref -> ?filename:string -> unit -> string option val set_highlight_timer : (unit -> 'a) -> unit diff --git a/ide/index_urls.txt b/ide/index_urls.txt deleted file mode 100644 index fea61809..00000000 --- a/ide/index_urls.txt +++ /dev/null @@ -1,563 +0,0 @@ -+,node.0.2.0.html#@default146 --,node.0.2.1.html#@default247 -2,node.1.2.9.html#@default514 -;,node.1.2.12.html#@default547 -?,node.1.0.6.html#@default358 -?,node.1.2.1.html#@default410 -&,node.0.2.0.html#@default164 -{A}+{B},node.0.2.0.html#@default174 -{x:A & (P x)},node.0.2.0.html#@default163 -{x:A | (P x)},node.0.2.0.html#@default157 -|,node.0.2.0.html#@default158 -A*B,node.0.2.0.html#@default150 -A+{B},node.0.2.0.html#@default178 -A+B,node.0.2.0.html#@default145 -Abort,node.1.1.0.html#@default385 -Absolute names,node.0.1.6.html#@default85 -Abstract,node.1.2.12.html#@default559 -Absurd,node.1.2.3.html#@default442 -Acc,node.0.2.0.html#@default215 -Acc_inv,node.0.2.0.html#@default216 -Acc_rec,node.0.2.0.html#@default217 -Add Abstract Ring,node.3.7.4.html#@default643 -Add Abstract Semi Ring,node.3.7.4.html#@default644 -Add Field,node.1.2.10.html#@default526 -Add LoadPath,node.1.0.4.html#@default338 -Add ML Path,node.1.0.4.html#@default342 -Add Morphism,node.3.8.2.html#@default647 -Add Printing If,node.0.1.1.html#@default67 -Add Printing Let,node.0.1.1.html#@default63 -Add Rec LoadPath,node.1.0.4.html#@default339 -Add Rec ML Path,node.1.0.4.html#@default343 -Add Ring,node.1.2.10.html#@default523 -Add Semi Ring,node.1.2.10.html#@default524 -Add Setoid,node.3.8.1.html#@default646 -All,node.0.2.0.html#@default110 -AllT,node.0.2.0.html#@default224 -Apply,node.1.2.2.html#@default427 -Apply ... with,node.1.2.2.html#@default428 -Arithmetical notations,node.0.2.1.html#@default244 -Arity,node.0.3.4.html#@default288 -Assert,node.1.2.2.html#@default433 -Associativity,node.2.0.1.html#@default571 -Assumption,node.1.2.2.html#@default412 -Auto,node.1.2.10.html#@default515 -AutoRewrite,node.1.2.10.html#@default528 -Axiom,node.0.0.2.html#@default24 -abstractions,node.0.0.1.html#@default16 -absurd,node.0.2.0.html#@default121 -absurd_set,node.0.2.0.html#@default188 -all,node.0.2.0.html#@default109 -allT,node.0.2.0.html#@default223 -and,node.0.2.0.html#@default99 -and_rec,node.0.2.0.html#@default189 -applications,node.0.0.1.html#@default18 -Back,node.1.0.5.html#@default348 -Bad Magic Number,node.1.0.3.html#@default331 -Begin Silent,node.1.0.7.html#@default366 -Binding list,node.1.2.2.html#@default441 -beta-reduction,node.0.3.2.html#@default274 -bool,node.0.2.0.html#@default135 -bool_choice,node.0.2.0.html#@default181 -byte-code,node.3.0.0.html#@default574 -Calculus of (Co)Inductive Constructions,node.0.3.html#@default255 -Canonical Structure,node.0.1.7.html#@default91 -Case,node.1.2.6.html#@default468 -Case ... with,node.1.2.6.html#@default469 -Cases,node.3.2.html#@default593 -Cases...of...end,node.0.0.1.html#@default21 -Cbv,node.1.2.4.html#@default445 -Cd,node.1.0.4.html#@default337 -Change,node.1.2.2.html#@default438 -Change ... in,node.1.2.2.html#@default440 -Chapter,node.0.1.3.html#@default73 -Check,node.1.0.1.html#@default308 -Choice,node.0.2.0.html#@default179 -Choice2,node.0.2.0.html#@default180 -CIC,node.0.3.html#@default254 -Clear,node.1.2.2.html#@default414 -ClearBody,node.1.2.2.html#@default415 -Coercion,node.3.3.5.html#@default601 -Coercion Local,node.3.3.5.html#@default602 -Coercions,node.0.1.8.html#@default92 -and sections,node.3.3.9.html#@default616 -classes,node.3.3.1.html#@default596 -FUNCLASS,node.3.3.2.html#@default597 -identity,node.3.3.3.html#@default599 -inheritance graph,node.3.3.4.html#@default600 -presentation,node.3.3.html#@default595 -SORTCLASS,node.3.3.2.html#@default598 -CoFixpoint,node.0.0.2.html#@default40 -CoInductive,node.0.0.2.html#@default38 -Comments,node.0.0.0.html#@default2 -Compare,node.1.2.8.html#@default489 -Compiled files,node.1.0.3.html#@default327 -Compute,node.1.2.4.html#@default447 -Connectives,node.0.2.0.html#@default94 -Constant,node.0.0.2.html#@default31 -Constructor,node.1.2.5.html#@default455 -Constructor ... with,node.1.2.5.html#@default456 -Context,node.0.3.1.html#@default263 -Contradiction,node.1.2.3.html#@default443 -Contributions,node.0.2.2.html#@default253 -Conversion rules,node.0.3.2.html#@default273 -Conversion tactics,node.1.2.4.html#@default444 -coqdep,node.3.1.1.html#@default582 -coq_Makefile,node.3.1.2.html#@default584 -coqmktop,node.3.1.0.html#@default579 -coq-tex,node.3.1.3.html#@default586 -coqweb,node.3.1.3.html#@default587 -Correctness,node.3.5.html#@default619 -Cut,node.1.2.2.html#@default434 -CutRewrite,node.1.2.7.html#@default482 -congr_eqT,node.0.2.0.html#@default241 -conj,node.0.2.0.html#@default100 -coqc,node.3.0.html#@default573 -coqtop,node.3.0.html#@default572 -Datatypes,node.0.2.0.html#@default132 -Debugger,node.3.1.0.html#@default580 -Decide Equality,node.1.2.8.html#@default488 -Declarations,node.0.0.2.html#@default23 -Declare ML Module,node.1.0.3.html#@default333 -Decompose,node.1.2.6.html#@default473 -Decompose Record,node.1.2.6.html#@default475 -Decompose Sum,node.1.2.6.html#@default474 -Defined,node.0.0.2.html#@default48 -Definition,node.0.0.2.html#@default33 -Definitions,node.0.0.2.html#@default29 -Dependencies,node.3.1.1.html#@default581 -Dependent Inversion,node.1.2.9.html#@default501 -Dependent Inversion ... with,node.1.2.9.html#@default503 -Dependent Inversion_clear,node.1.2.9.html#@default502 -Dependent Inversion_clear ... with,node.1.2.9.html#@default504 -Dependent Rewrite ->,node.1.2.8.html#@default495 -Dependent Rewrite <-,node.1.2.8.html#@default496 -Derive Dependent Inversion,node.1.2.9.html#@default511 -Derive Dependent Inversion_clear,node.1.2.9.html#@default512 -Derive Inversion,node.1.2.9.html#@default508 -Derive Inversion_clear,node.1.2.9.html#@default509 -Derive Inversion_clear ... with,node.1.2.9.html#@default510 -Destruct,node.1.2.6.html#@default466 -Discriminate,node.1.2.8.html#@default490 -DiscrR,node.0.2.1.html#@default250 -Do,node.1.2.12.html#@default542 -Double Induction,node.1.2.6.html#@default472 -Drop,node.1.0.7.html#@default365 -delta-reduction,node.0.0.2.html#@default30 -EApply,node.1.2.2.html#@default429 -EAuto,node.1.2.10.html#@default517 -Elim ... using,node.1.2.6.html#@default463 -Elim ... with,node.1.2.6.html#@default462 -Singleton elimination,node.0.3.4.html#@default294 -Elimination sorts,node.0.3.4.html#@default291 -ElimType,node.1.2.6.html#@default464 -Emacs,node.3.1.5.html#@default589 -EmptyT,node.0.2.0.html#@default233 -End,node.0.1.3.html#@default74 -End Silent,node.1.0.7.html#@default368 -Environment,node.0.0.2.html#@default32 -Environment variables,node.3.0.3.html#@default577 -Equality,node.0.2.0.html#@default118 -Eval,node.1.0.1.html#@default309 -EX,node.0.2.0.html#@default113 -EXT,node.0.2.0.html#@default229 -Ex,node.0.2.0.html#@default112 -Ex2,node.0.2.0.html#@default116 -Exact,node.1.2.1.html#@default408 -Exc,node.0.2.0.html#@default182 -Except,node.0.2.0.html#@default187 -Exists,node.1.2.5.html#@default458 -Explicitation of implicit arguments,node.0.1.7.html#@default88 -ExT,node.0.2.0.html#@default228 -ExT2,node.0.2.0.html#@default231 -Extensive grammars,node.1.0.6.html#@default362 -Extract Constant,node.3.6.1.html#@default637 -Extract Inductive,node.3.6.1.html#@default638 -Extraction,node.3.6.html#@default623 -Extraction,node.1.0.1.html#@default310 -Extraction Inline,node.3.6.1.html#@default633 -Extraction Language,node.3.6.1.html#@default628 -Extraction Module,node.3.6.0.html#@default626 -Extraction NoInline,node.3.6.1.html#@default634 -eq,node.0.2.0.html#@default119 -eq_add_S,node.0.2.0.html#@default193 -eq_ind_r,node.0.2.0.html#@default126 -eq_rec,node.0.2.0.html#@default186 -eq_rec_r,node.0.2.0.html#@default127 -eq_rect,node.0.2.0.html#@default128 -eq_rect_r,node.0.2.0.html#@default129 -eq_S,node.0.2.0.html#@default190 -eqT,node.0.2.0.html#@default236 -eqT_ind_r,node.0.2.0.html#@default242 -eqT_rec_r,node.0.2.0.html#@default243 -error,node.0.2.0.html#@default184 -ex,node.0.2.0.html#@default111 -ex2,node.0.2.0.html#@default115 -ex_intro,node.0.2.0.html#@default114 -ex_intro2,node.0.2.0.html#@default117 -exist,node.0.2.0.html#@default160 -exist2,node.0.2.0.html#@default162 -existS,node.0.2.0.html#@default166 -existS2,node.0.2.0.html#@default170 -exT,node.0.2.0.html#@default227 -exT2,node.0.2.0.html#@default232 -exT_intro,node.0.2.0.html#@default230 -Fact,node.0.0.2.html#@default44 -Fail,node.1.2.12.html#@default540 -False,node.0.2.0.html#@default97 -False_rec,node.0.2.0.html#@default185 -Field,node.1.2.10.html#@default525 -First,node.1.2.12.html#@default553 -Fix,node.0.3.4.html#@default298 -Fix_F,node.0.2.0.html#@default219 -Fix_F_eq,node.0.2.0.html#@default222 -Fix_F_inv,node.0.2.0.html#@default221 -Fixpoint,node.0.0.2.html#@default39 -Focus,node.1.1.1.html#@default392 -Fold,node.1.2.4.html#@default453 -Fourier,node.1.2.10.html#@default527 -Fst,node.0.2.0.html#@default155 -f_equal,node.0.2.0.html#@default124 -f_equali,node.0.2.0.html#@default130 -false,node.0.2.0.html#@default137 -fix_eq,node.0.2.0.html#@default220 -fst,node.0.2.0.html#@default153 -Gallina,node.0.0.html#@default0 -gallina,node.3.1.6.html#@default591 -Generalize,node.1.2.2.html#@default436 -Generalize Dependent,node.1.2.2.html#@default437 -Global Variable,node.3.5.2.html#@default620 -Goal,node.0.0.2.html#@default50 -Grammar,node.1.0.6.html#@default361 -ge,node.0.2.0.html#@default208 -gen,node.0.2.0.html#@default226 -goal,node.1.2.html#@default405 -gt,node.0.2.0.html#@default209 -Head normal form,node.0.3.2.html#@default286 -Hint,node.1.2.11.html#@default531 -Hint Rewrite,node.1.2.10.html#@default529 -Hints databases,node.1.2.11.html#@default530 -Hints Immediate,node.1.2.11.html#@default533 -Hints Resolve,node.1.2.11.html#@default532 -Hints Unfold,node.1.2.11.html#@default534 -Hnf,node.1.2.4.html#@default449 -HTML,node.3.1.4.html#@default588 -Hypothesis,node.0.0.2.html#@default28 -I,node.0.2.0.html#@default96 -Identity Coercion,node.3.3.5.html#@default605 -Idtac,node.1.2.12.html#@default538 -IF,node.0.2.0.html#@default107 -proof of,node.3.5.html#@default618 -Implicit Arguments Off,node.1.0.6.html#@default355 -Implicit Arguments On,node.1.0.6.html#@default354 -Implicits,node.1.0.6.html#@default356 -Induction,node.1.2.6.html#@default465 -Inductive,node.0.0.2.html#@default36 -Inductive definitions,node.0.0.2.html#@default35 -Infix,node.1.0.6.html#@default363 -Info,node.1.2.12.html#@default557 -Injection,node.1.2.8.html#@default492 -Inspect,node.1.0.0.html#@default305 -Intro,node.1.2.2.html#@default418 -Intro ... after,node.1.2.2.html#@default426 -Intro after,node.1.2.2.html#@default425 -Intros,node.1.2.2.html#@default422 -Intros pattern,node.1.2.6.html#@default471 -Intros until,node.1.2.2.html#@default423 -Intuition,node.1.2.10.html#@default520 -Inversion,node.1.2.9.html#@default497 -Inversion ... in,node.1.2.9.html#@default499 -Inversion ... using,node.1.2.9.html#@default505 -Inversion ... using ... in,node.1.2.9.html#@default506 -Inversion_clear,node.1.2.9.html#@default498 -Inversion_clear ... in,node.1.2.9.html#@default500 -IsSucc,node.0.2.0.html#@default195 -if ... then ... else,node.0.1.1.html#@default55 -iff,node.0.2.0.html#@default106 -implicit arguments,node.0.1.7.html#@default86 -inl,node.0.2.0.html#@default147 -inleft,node.0.2.0.html#@default176 -inr,node.0.2.0.html#@default148 -inright,node.0.2.0.html#@default177 -iota-reduction,node.0.3.2.html#@default275 -LApply,node.1.2.2.html#@default430 -Lazy,node.1.2.4.html#@default446 -Left,node.1.2.5.html#@default459 -Lemma,node.0.0.2.html#@default42 -LetTac,node.1.2.2.html#@default431 -Lexical conventions,node.0.0.0.html#@default1 -Libraries,node.0.1.5.html#@default82 -Load,node.1.0.2.html#@default325 -Load Verbose,node.1.0.2.html#@default326 -Loadpath,node.1.0.4.html#@default335 -Local,node.0.0.2.html#@default34 -Local definitions,node.0.0.1.html#@default19 -Locate,node.1.0.1.html#@default323 -Locate Library,node.1.0.4.html#@default346 -Logical paths,node.0.1.5.html#@default83 -le,node.0.2.0.html#@default204 -le_n,node.0.2.0.html#@default205 -le_S,node.0.2.0.html#@default206 -left,node.0.2.0.html#@default172 -let ... in,node.0.1.1.html#@default56 -let-in,node.0.0.1.html#@default20 -local context,node.1.1.html#@default372 -lt,node.0.2.0.html#@default207 -Makefile,node.3.1.2.html#@default583 -Man pages,node.3.1.7.html#@default592 -ML-like patterns,node.0.1.1.html#@default54 -Module,node.0.1.4.html#@default75 -Module Type,node.0.1.4.html#@default78 -Move,node.1.2.2.html#@default416 -Mutual Inductive,node.0.0.2.html#@default37 -mult,node.0.2.0.html#@default201 -mult_n_O,node.0.2.0.html#@default202 -mult_n_Sm,node.0.2.0.html#@default203 -NewDestruct,node.1.2.6.html#@default467 -NewInduction,node.1.2.6.html#@default461 -None,node.0.2.0.html#@default143 -Normal form,node.0.3.2.html#@default285 -Notation,node.2.0.0.html#@default569 -Notations for real numbers,node.0.2.1.html#@default249 -n_Sn,node.0.2.0.html#@default197 -nat,node.0.2.0.html#@default138 -nat_case,node.0.2.0.html#@default210 -nat_double_ind,node.0.2.0.html#@default211 -native code,node.3.0.0.html#@default575 -not,node.0.2.0.html#@default98 -not_eq_S,node.0.2.0.html#@default194 -notT,node.0.2.0.html#@default235 -O,node.0.2.0.html#@default139 -O_S,node.0.2.0.html#@default196 -Omega,node.1.2.10.html#@default521 -Opaque,node.1.0.1.html#@default311 -Options of the command line,node.3.0.4.html#@default578 -Orelse,node.1.2.12.html#@default544 -option,node.0.2.0.html#@default141 -or,node.0.2.0.html#@default103 -or_introl,node.0.2.0.html#@default104 -or_intror,node.0.2.0.html#@default105 -Parameter,node.0.0.2.html#@default25 -Pattern,node.1.2.4.html#@default454 -Peano's arithmetic notations,node.0.2.1.html#@default248 -Pose,node.1.2.2.html#@default432 -Positivity,node.0.3.4.html#@default287 -Precedences,node.2.0.1.html#@default570 -Pretty printing,node.1.0.6.html#@default360 -Print,node.1.0.0.html#@default302 -Print All,node.1.0.0.html#@default304 -Print Classes,node.3.3.6.html#@default606 -Print Coercion Paths,node.3.3.6.html#@default609 -Print Coercions,node.3.3.6.html#@default607 -Print Extraction Inline,node.3.6.1.html#@default635 -Print Graph,node.3.3.6.html#@default608 -Print Hint,node.1.2.11.html#@default535 -Print HintDb,node.1.2.11.html#@default536 -Print LoadPath,node.1.0.4.html#@default341 -Print ML Modules,node.1.0.3.html#@default334 -Print ML Path,node.1.0.4.html#@default344 -Print Module,node.0.1.4.html#@default80 -Print Module Type,node.0.1.4.html#@default81 -Print Modules,node.1.0.3.html#@default332 -Print Proof,node.1.0.0.html#@default303 -Print Section,node.1.0.0.html#@default306 -Print Table Printing If,node.0.1.1.html#@default70 -Print Table Printing Let,node.0.1.1.html#@default66 -Programming,node.0.2.0.html#@default131 -Prolog,node.1.2.10.html#@default518 -Prompt,node.1.1.html#@default371 -Proof,node.0.0.2.html#@default45 -Proof editing,node.1.1.html#@default370 -Proof General,node.3.1.5.html#@default590 -Proof term,node.1.1.html#@default373 -Prop,node.0.0.1.html#@default11 -Pwd,node.1.0.4.html#@default336 -pair,node.0.2.0.html#@default152 -plus,node.0.2.0.html#@default198 -plus_n_O,node.0.2.0.html#@default199 -plus_n_Sm,node.0.2.0.html#@default200 -pred,node.0.2.0.html#@default191 -pred_Sn,node.0.2.0.html#@default192 -prod,node.0.2.0.html#@default149 -products,node.0.0.1.html#@default17 -proj1,node.0.2.0.html#@default101 -proj2,node.0.2.0.html#@default102 -projS1,node.0.2.0.html#@default167 -projS2,node.0.2.0.html#@default168 -Qed,node.0.0.2.html#@default47 -Qualified identifiers,node.0.1.6.html#@default84 -Quantifiers,node.0.2.0.html#@default108 -Quit,node.1.0.7.html#@default364 -Quote,node.1.2.9.html#@default513 -?,node.0.1.7.html#@default90 -Read Module,node.1.0.3.html#@default328 -Record,node.0.1.0.html#@default52 -Recursion,node.0.2.0.html#@default213 -Recursive arguments,node.0.3.4.html#@default300 -Recursive Extraction,node.3.6.0.html#@default625 -Recursive Extraction Module,node.3.6.0.html#@default627 -Red,node.1.2.4.html#@default448 -Refine,node.1.2.1.html#@default409 -Reflexivity,node.1.2.7.html#@default484 -Remark,node.0.0.2.html#@default43 -Remove LoadPath,node.1.0.4.html#@default340 -Remove Printing If,node.0.1.1.html#@default68 -Remove Printing Let,node.0.1.1.html#@default64 -Rename,node.1.2.2.html#@default417 -Replace ... with,node.1.2.7.html#@default483 -Require,node.1.0.3.html#@default329 -Require Export,node.1.0.3.html#@default330 -Reset,node.1.0.5.html#@default347 -Reset Extraction Inline,node.3.6.1.html#@default636 -Reset Initial,node.1.0.5.html#@default350 -Resource file,node.3.0.2.html#@default576 -Restart,node.1.1.1.html#@default391 -Restore State,node.1.0.5.html#@default349 -Resume,node.1.1.0.html#@default387 -Rewrite,node.1.2.7.html#@default476 -Rewrite ->,node.1.2.7.html#@default477 -Rewrite -> ... in,node.1.2.7.html#@default480 -Rewrite <-,node.1.2.7.html#@default478 -Rewrite <- ... in,node.1.2.7.html#@default481 -Rewrite ... in,node.1.2.7.html#@default479 -Right,node.1.2.5.html#@default460 -Ring,node.1.2.10.html#@default522 -refl_eqT,node.0.2.0.html#@default237 -refl_equal,node.0.2.0.html#@default120 -right,node.0.2.0.html#@default173 -S,node.0.2.0.html#@default140 -Save,node.0.0.2.html#@default49 -Scheme,node.1.2.13.html#@default561 -Script file,node.1.0.2.html#@default324 -Search,node.1.0.1.html#@default313 -Search ... inside ...,node.1.0.1.html#@default317 -Search ... outside ...,node.1.0.1.html#@default320 -SearchAbout,node.1.0.1.html#@default314 -SearchPattern,node.1.0.1.html#@default315 -SearchPattern ... outside ...,node.1.0.1.html#@default321 -SearchRewrite,node.1.0.1.html#@default316 -SearchRewrite ... inside ...,node.1.0.1.html#@default319 -SearchRewrite ... outside ...,node.1.0.1.html#@default322 -Section,node.0.1.3.html#@default72 -Sections,node.0.1.3.html#@default71 -Set,node.0.0.1.html#@default10 -Set Extraction AutoInline,node.3.6.1.html#@default631 -Set Extraction Optimize,#@default629 -Set Hyps_limit,node.1.1.2.html#@default402 -Set Implicit Arguments,node.0.1.7.html#@default87 -Set Printing Coercion,node.3.3.7.html#@default612 -Set Printing Coercions,node.3.3.7.html#@default610 -Set Printing Synth,node.0.1.1.html#@default60 -Set Printing Wildcard,node.0.1.1.html#@default57 -Set Undo,node.1.1.1.html#@default389 -Setoid_replace,node.3.8.html#@default645 -Setoid_rewrite,node.3.8.3.html#@default649 -Show,node.1.1.2.html#@default394 -Show Conjectures,node.1.1.2.html#@default399 -Show Implicits,node.1.1.2.html#@default395 -Show Intro,node.1.1.2.html#@default400 -Show Intros,node.1.1.2.html#@default401 -Show Programs,node.3.5.2.html#@default621 -Show Proof,node.1.1.2.html#@default398 -Show Script,node.1.1.2.html#@default396 -Show Tree,node.1.1.2.html#@default397 -Silent mode,node.1.0.7.html#@default367 -Simpl,node.1.2.4.html#@default450 -Simple Inversion,node.1.2.9.html#@default507 -Simplify_eq,node.1.2.8.html#@default494 -Small inductive type,node.0.3.4.html#@default292 -Snd,node.0.2.0.html#@default156 -Solve,node.1.2.12.html#@default555 -Some,node.0.2.0.html#@default142 -Sorts,node.0.0.1.html#@default8 -Split,node.1.2.5.html#@default457 -SplitAbsolu,node.0.2.1.html#@default251 -SplitRmult,node.0.2.1.html#@default252 -Strong elimination,node.0.3.4.html#@default293 -Structure,node.3.3.8.html#@default615 -Subst,node.1.2.7.html#@default487 -Substitution,node.0.3.0.html#@default262 -Suspend,node.1.1.0.html#@default386 -Symmetry,node.1.2.7.html#@default485 -Syntactic Definition,node.0.1.7.html#@default89 -Syntax,node.1.0.6.html#@default359 -sig,node.0.2.0.html#@default159 -sig2,node.0.2.0.html#@default161 -sigS,node.0.2.0.html#@default165 -sigS2,node.0.2.0.html#@default169 -snd,node.0.2.0.html#@default154 -sort,node.0.0.1.html#@default7 -specif,node.0.0.1.html#@default14 -subgoal,node.1.2.html#@default406 -sum,node.0.2.0.html#@default144 -sum_eqT,node.0.2.0.html#@default238 -sumbool,node.0.2.0.html#@default171 -sumor,node.0.2.0.html#@default175 -sym_eq,node.0.2.0.html#@default122 -sym_not_eq,node.0.2.0.html#@default125 -sym_not_eqT,node.0.2.0.html#@default239 -Tactic Definition,node.1.2.14.html#@default563 -Tacticals,node.1.2.12.html#@default537 -Do,node.1.2.12.html#@default543 -Fail,node.1.2.12.html#@default541 -First,node.1.2.12.html#@default554 -Solve,node.1.2.12.html#@default556 -Idtac,node.1.2.12.html#@default539 -Info,node.1.2.12.html#@default558 -Orelse,node.1.2.12.html#@default545 -Repeat,node.1.2.12.html#@default546 -Try,node.1.2.12.html#@default552 -Tactics,node.1.2.html#@default404 -Tauto,node.1.2.10.html#@default519 -Terms,node.0.0.1.html#@default5 -Test Printing If,node.0.1.1.html#@default69 -Test Printing Let,node.0.1.1.html#@default65 -Test Printing Synth,node.0.1.1.html#@default62 -Test Printing Wildcard,node.0.1.1.html#@default59 -Theorem,node.0.0.2.html#@default41 -Theories,node.0.2.html#@default93 -Time,node.1.0.7.html#@default369 -Transitivity,node.1.2.7.html#@default486 -Transparent,node.1.0.1.html#@default312 -Trivial,node.1.2.10.html#@default516 -True,node.0.2.0.html#@default95 -Try,node.1.2.12.html#@default551 -Type,node.0.0.1.html#@default9 -Type of constructor,node.0.3.4.html#@default289 -Typing rules,node.0.3.1.html#@default265 -Ax,node.0.3.1.html#@default266 -Cases,node.0.3.4.html#@default296 -Const,node.0.3.1.html#@default268 -Conv,node.0.3.2.html#@default282 -Fix,node.0.3.4.html#@default299 -Lam,node.0.3.1.html#@default270 -Let,node.0.3.1.html#@default272 -Prod,node.0.3.1.html#@default269 -Var,node.0.3.1.html#@default267 -tactic macros,node.1.2.14.html#@default562 -trans_eq,node.0.2.0.html#@default123 -trans_eqT,node.0.2.0.html#@default240 -true,node.0.2.0.html#@default136 -tt,node.0.2.0.html#@default134 -Undo,node.1.1.1.html#@default388 -Unfocus,node.1.1.1.html#@default393 -Unfold,node.1.2.4.html#@default451 -Unfold ... in,node.1.2.4.html#@default452 -UnitT,node.0.2.0.html#@default234 -Unset Extraction AutoInline,node.3.6.1.html#@default632 -Unset Extraction Optimize,#@default630 -Unset Hyps_limit,node.1.1.2.html#@default403 -Unset Implicit Arguments,node.1.0.6.html#@default353 -Unset Printing Coercion,node.3.3.7.html#@default613 -Unset Printing Coercions,node.3.3.7.html#@default611 -Unset Printing Synth,node.0.1.1.html#@default61 -Unset Printing Wildcard,node.0.1.1.html#@default58 -Unset Undo,node.1.1.1.html#@default390 -unit,node.0.2.0.html#@default133 -Variable,node.0.0.2.html#@default26 -Variables,node.0.0.2.html#@default27 -value,node.0.2.0.html#@default183 -Well founded induction,node.0.2.0.html#@default214 -Well foundedness,node.0.2.0.html#@default212 -Write State,node.1.0.5.html#@default351 -well_founded,node.0.2.0.html#@default218 diff --git a/ide/preferences.ml b/ide/preferences.ml index c01fa602..444b2c2b 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 9350 2006-11-07 15:04:42Z notin $ *) +(* $Id: preferences.ml 11058 2008-06-06 08:21:03Z herbelin $ *) open Configwin open Printf @@ -73,10 +73,11 @@ type pref = mutable modifier_for_navigation : Gdk.Tags.modifier list; mutable modifier_for_templates : Gdk.Tags.modifier list; mutable modifier_for_tactics : Gdk.Tags.modifier list; + mutable modifier_for_display : Gdk.Tags.modifier list; mutable modifiers_valid : Gdk.Tags.modifier list; - mutable cmd_browse : string * string; - mutable cmd_editor : string * string; + mutable cmd_browse : string; + mutable cmd_editor : string; mutable text_font : Pango.font_description; @@ -95,6 +96,8 @@ type pref = mutable auto_complete : bool; mutable stop_before : bool; mutable lax_syntax : bool; + mutable vertical_tabs : bool; + mutable opposite_tabs : bool; } let (current:pref ref) = @@ -108,7 +111,7 @@ let (current:pref ref) = global_auto_revert = false; global_auto_revert_delay = 10000; - auto_save = false; + auto_save = true; auto_save_delay = 10000; auto_save_name = "#","#"; @@ -122,16 +125,15 @@ let (current:pref ref) = modifier_for_navigation = [`CONTROL; `MOD1]; modifier_for_templates = [`CONTROL; `SHIFT]; modifier_for_tactics = [`CONTROL; `MOD1]; + modifier_for_display = [`MOD1;`SHIFT]; modifiers_valid = [`SHIFT; `CONTROL; `MOD1]; - cmd_browse = Options.browser_cmd_fmt; - cmd_editor = - if Sys.os_type = "Win32" - then "NOTEPAD ", "" - else "emacs ", ""; + cmd_browse = Flags.browser_cmd_fmt; + cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s"; - text_font = Pango.Font.from_string "sans 12"; +(* text_font = Pango.Font.from_string "sans 12";*) + text_font = Pango.Font.from_string "Monospace 10"; doc_url = "http://coq.inria.fr/doc/"; library_url = "http://coq.inria.fr/library/"; @@ -147,7 +149,9 @@ let (current:pref ref) = *) auto_complete = false; stop_before = true; - lax_syntax = true + lax_syntax = true; + vertical_tabs = false; + opposite_tabs = false; } @@ -192,10 +196,12 @@ let save_pref () = (List.map mod_to_str p.modifier_for_templates) ++ add "modifier_for_tactics" (List.map mod_to_str p.modifier_for_tactics) ++ + add "modifier_for_display" + (List.map mod_to_str p.modifier_for_display) ++ add "modifiers_valid" (List.map mod_to_str p.modifiers_valid) ++ - add "cmd_browse" [fst p.cmd_browse; snd p.cmd_browse] ++ - add "cmd_editor" [fst p.cmd_editor; snd p.cmd_editor] ++ + add "cmd_browse" [p.cmd_browse] ++ + add "cmd_editor" [p.cmd_editor] ++ add "text_font" [Pango.Font.to_string p.text_font] ++ @@ -211,6 +217,8 @@ let save_pref () = add "auto_complete" [string_of_bool p.auto_complete] ++ add "stop_before" [string_of_bool p.stop_before] ++ add "lax_syntax" [string_of_bool p.lax_syntax] ++ + add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ + add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." @@ -226,6 +234,9 @@ let load_pref () = let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in let set_int k f = set_hd k (fun v -> f (int_of_string v)) in let set_pair k f = set k (function [v1;v2] -> f v1 v2 | _ -> raise Exit) in + let set_command_with_pair_compat k f = + set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) + in set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); set_hd "cmd_make" (fun v -> np.cmd_make <- v); set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); @@ -248,10 +259,12 @@ let load_pref () = (fun v -> np.modifier_for_templates <- List.map str_to_mod v); set "modifier_for_tactics" (fun v -> np.modifier_for_tactics <- List.map str_to_mod v); + set "modifier_for_display" + (fun v -> np.modifier_for_display <- List.map str_to_mod v); set "modifiers_valid" (fun v -> np.modifiers_valid <- List.map str_to_mod v); - set_pair "cmd_browse" (fun v1 v2 -> np.cmd_browse <- (v1,v2)); - set_pair "cmd_editor" (fun v1 v2 -> np.cmd_editor <- (v1,v2)); + set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v); + set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v); set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v); set_hd "doc_url" (fun v -> np.doc_url <- v); set_hd "library_url" (fun v -> np.library_url <- v); @@ -265,9 +278,11 @@ let load_pref () = set_bool "auto_complete" (fun v -> np.auto_complete <- v); set_bool "stop_before" (fun v -> np.stop_before <- v); set_bool "lax_syntax" (fun v -> np.lax_syntax <- v); + set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); + set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); current := np; (* - Format.printf "in laod_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); + Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) with e -> prerr_endline ("Could not load preferences ("^ @@ -281,7 +296,7 @@ let split_string_format s = pre,post with Not_found -> s,"" -let configure () = +let configure ?(apply=(fun () -> ())) () = let cmd_coqc = string ~f:(fun s -> !current.cmd_coqc <- s) @@ -405,6 +420,18 @@ let configure () = "Relax read-only constraint at end of command" !current.lax_syntax in + let vertical_tabs = + bool + ~f:(fun s -> !current.vertical_tabs <- s) + "Vertical tabs" !current.vertical_tabs + in + + let opposite_tabs = + bool + ~f:(fun s -> !current.opposite_tabs <- s) + "Tabs on opposite side" !current.opposite_tabs + in + let encodings = combo "File charset encoding " @@ -426,10 +453,14 @@ let configure () = (if !current.encoding_use_utf8 then "UTF-8" else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) in + let help_string = + "Press a set of modifiers and an extra key together (needs then a restart to apply!)" + in let modifier_for_tactics = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_tactics <- l) + ~help:help_string "Modifiers for Tactics Menu" !current.modifier_for_tactics in @@ -437,6 +468,7 @@ let configure () = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_templates <- l) + ~help:help_string "Modifiers for Templates Menu" !current.modifier_for_templates in @@ -444,35 +476,53 @@ let configure () = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_navigation <- l) + ~help:help_string "Modifiers for Navigation Menu" !current.modifier_for_navigation in + let modifier_for_display = + modifiers + ~allow:!current.modifiers_valid + ~f:(fun l -> !current.modifier_for_display <- l) + ~help:help_string + "Modifiers for Display Menu" + !current.modifier_for_display + in let modifiers_valid = modifiers ~f:(fun l -> !current.modifiers_valid <- l) "Allowed modifiers" !current.modifiers_valid in - let mod_msg = - string - "Needs restart to apply!" - ~editable:false - "" - in - let cmd_editor = - string - ~f:(fun s -> !current.cmd_editor <- split_string_format s) + let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in + combo ~help:"(%s for file name)" "External editor" - ((fst !current.cmd_editor)^"%s"^(snd !current.cmd_editor)) + ~f:(fun s -> !current.cmd_editor <- s) + ~new_allowed: true + (predefined@[if List.mem !current.cmd_editor predefined then "" + else !current.cmd_editor]) + !current.cmd_editor in - let cmd_browse = - string - ~f:(fun s -> !current.cmd_browse <- split_string_format s) + let cmd_browse = + let predefined = [ + "netscape -remote \"openURL(%s)\""; + "mozilla -remote \"openURL(%s)\""; + "firefox -remote \"openURL(%s,new-tab)\" || firefox %s &"; + "firefox -remote \"openURL(%s,new-windows)\" || firefox %s &"; + "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"; + "C:\\PROGRA~1\\INTERN~1\\IEXPLORE %s"; + "open -a Safari %s &" + ] in + combo ~help:"(%s for url)" - " Browser" - ((fst !current.cmd_browse)^"%s"^(snd !current.cmd_browse)) + "Browser" + ~f:(fun s -> !current.cmd_browse <- s) + ~new_allowed: true + (predefined@[if List.mem !current.cmd_browse predefined then "" + else !current.cmd_browse]) + !current.cmd_browse in let doc_url = string ~f:(fun s -> !current.doc_url <- s) " Manual URL" !current.doc_url in @@ -496,7 +546,8 @@ let configure () = "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax] in + let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; + vertical_tabs;opposite_tabs] in (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) @@ -520,14 +571,14 @@ let configure () = [automatic_tactics]); Section("Shortcuts", [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_navigation;mod_msg]); + modifier_for_templates; modifier_for_display; modifier_for_navigation]); Section("Misc", misc)] in (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - let x = edit ~width:500 "Customizations" cmds in + let x = edit ~apply ~width:500 "Customizations" cmds in (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) diff --git a/ide/preferences.mli b/ide/preferences.mli index c3e26f50..d7f32380 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: preferences.mli 9240 2006-10-13 17:51:11Z notin $ i*) +(*i $Id: preferences.mli 11009 2008-05-28 13:58:33Z jnarboux $ i*) type pref = { @@ -32,10 +32,11 @@ type pref = mutable modifier_for_navigation : Gdk.Tags.modifier list; mutable modifier_for_templates : Gdk.Tags.modifier list; mutable modifier_for_tactics : Gdk.Tags.modifier list; + mutable modifier_for_display : Gdk.Tags.modifier list; mutable modifiers_valid : Gdk.Tags.modifier list; - mutable cmd_browse : string * string; - mutable cmd_editor : string * string; + mutable cmd_browse : string; + mutable cmd_editor : string; mutable text_font : Pango.font_description; @@ -54,6 +55,8 @@ type pref = mutable auto_complete : bool; mutable stop_before : bool; mutable lax_syntax : bool; + mutable vertical_tabs : bool; + mutable opposite_tabs : bool; } val save_pref : unit -> unit @@ -61,7 +64,7 @@ val load_pref : unit -> unit val current : pref ref -val configure : unit -> unit +val configure : ?apply:(unit -> unit) -> unit -> unit val change_font : ( Pango.font_description -> unit) ref val show_toolbar : (bool -> unit) ref diff --git a/ide/utf8.v b/ide/utf8.v deleted file mode 100644 index 574f2e65..00000000 --- a/ide/utf8.v +++ /dev/null @@ -1,56 +0,0 @@ -(* -*- coding:utf-8 -* *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* y) (at level 90, right associativity): type_scope. -Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. -Notation "⌉ x" := (~x) (at level 75, right associativity) : type_scope. - - -(* Abstraction *) -(* Not nice -Notation "'λ' x : T , y" := ([x:T] y) (at level 1, x,T,y at level 10). -Notation "'λ' x := T , y" := ([x:=T] y) (at level 1, x,T,y at level 10). -*) - -(* Arithmetic *) -Notation "x ≤ y" := (le x y) (at level 70, no associativity). -Notation "x ≥ y" := (ge x y) (at level 70, no associativity). - -(* test *) -(* -Goal ∀ x, True -> (∃ y , x ≥ y + 1) ∨ x ≤ 0. -*) - -(* Integer Arithmetic *) -(* TODO -Notation "x ≤ y" := (Zle x y) (at level 1, y at level 10). -*) diff --git a/ide/utils/config_file.ml b/ide/utils/config_file.ml index 30eb0111..d972639f 100644 --- a/ide/utils/config_file.ml +++ b/ide/utils/config_file.ml @@ -23,7 +23,7 @@ (* *) (*********************************************************************************) -(* $Id: config_file.ml 8618 2006-03-08 11:44:47Z notin $ *) +(* $Id: config_file.ml 10348 2007-12-06 17:36:14Z aspiwack $ *) (* TODO *) (* section comments *) @@ -552,7 +552,7 @@ class filename_cp = string_cp (* ******************************************************************************** *) -(******************** Backward compatibility with module Options ****************** *) +(******************** Backward compatibility with module Flags.****************** *) (* ******************************************************************************** *) type 'a option_class = 'a wrappers diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 240fd829..3ab3823d 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -364,7 +364,7 @@ class string_param_box param (tt:GData.tooltips) = let _ = dbg "string_param_box" in let hbox = GPack.hbox () in let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in - let wl = GMisc.label ~text: param.string_label ~packing: wev#add () in + let _wl = GMisc.label ~text: param.string_label ~packing: wev#add () in let we = GEdit.entry ~editable: param.string_editable ~packing: (hbox#pack ~expand: param.string_expand ~padding: 2) @@ -396,7 +396,7 @@ class combo_param_box param (tt:GData.tooltips) = let _ = dbg "combo_param_box" in let hbox = GPack.hbox () in let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in - let wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in + let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in let wc = GEdit.combo ~popdown_strings: param.combo_choices ~value_in_list: (not param.combo_new_allowed) @@ -754,9 +754,7 @@ class hotkey_param_box param (tt:GData.tooltips) = let _ = dbg "hotkey_param_box" in let hbox = GPack.hbox () in let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in - let wl = GMisc.label ~text: param.hk_label - ~packing: wev#add () - in + let _wl = GMisc.label ~text: param.hk_label ~packing: wev#add () in let we = GEdit.entry ~editable: false ~packing: (hbox#pack ~expand: param.hk_expand ~padding: 2) @@ -805,9 +803,7 @@ class hotkey_param_box param (tt:GData.tooltips) = class modifiers_param_box param = let hbox = GPack.hbox () in let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in - let wl = GMisc.label ~text: param.md_label - ~packing: wev#add () - in + let _wl = GMisc.label ~text: param.md_label ~packing: wev#add () in let we = GEdit.entry ~editable: false ~packing: (hbox#pack ~expand: param.md_expand ~padding: 2) diff --git a/ide/utils/uoptions.ml b/ide/utils/uoptions.ml index 416f5769..aa3b42cd 100644 --- a/ide/utils/uoptions.ml +++ b/ide/utils/uoptions.ml @@ -24,7 +24,7 @@ (** Simple options: This will enable very simple configuration, by a mouse-based configurator. - Options will be defined by a special function, which will also check + Flags.will be defined by a special function, which will also check if a value has been provided by the user in its .gwmlrc file. The .gwmlrc will be created by a dedicated tool, which could be used to generate both .gwmlrc and .efunsrc files. @@ -151,7 +151,7 @@ let opfile.file_rc) with Not_found -> default_value | e -> - Printf.printf "Options.define_option, for option %s: " + Printf.printf "Flags.define_option, for option %s: " (match option_name with [] -> "???" | name :: _ -> name); @@ -344,7 +344,7 @@ let value_to_string v = StringValue s -> s | IntValue i -> string_of_int i | FloatValue f -> string_of_float f - | _ -> failwith "Options: not a string option" + | _ -> failwith "Flags. not a string option" ;; let string_to_value s = StringValue s;; @@ -353,7 +353,7 @@ let value_to_int v = match v with StringValue s -> int_of_string s | IntValue i -> i - | _ -> failwith "Options: not an int option" + | _ -> failwith "Flags. not an int option" ;; let int_to_value i = IntValue i;; @@ -375,7 +375,7 @@ let value_to_bool v = StringValue s -> bool_of_string s | IntValue v when v = 0 -> false | IntValue v when v = 1 -> true - | _ -> failwith "Options: not a bool option" + | _ -> failwith "Flags. not a bool option" ;; let bool_to_value i = StringValue (string_of_bool i);; @@ -383,7 +383,7 @@ let value_to_float v = match v with StringValue s -> float_of_string s | FloatValue f -> f - | _ -> failwith "Options: not a float option" + | _ -> failwith "Flags. not a float option" ;; let float_to_value i = FloatValue i;; @@ -392,7 +392,7 @@ let value_to_string2 v = match v with List [s1; s2] | SmallList [s1;s2] -> value_to_string s1, value_to_string s2 - | _ -> failwith "Options: not a string2 option" + | _ -> failwith "Flags. not a string2 option" ;; let string2_to_value (s1, s2) = SmallList [StringValue s1; StringValue s2];; @@ -401,10 +401,10 @@ let value_to_list v2c v = match v with List l | SmallList l -> List.rev (List.rev_map v2c l) | StringValue s -> failwith (Printf.sprintf - "Options: not a list option (StringValue [%s])" s) - | FloatValue _ -> failwith "Options: not a list option (FloatValue)" - | IntValue _ -> failwith "Options: not a list option (IntValue)" - | Module _ -> failwith "Options: not a list option (Module)" + "Flags. not a list option (StringValue [%s])" s) + | FloatValue _ -> failwith "Flags. not a list option (FloatValue)" + | IntValue _ -> failwith "Flags. not a list option (IntValue)" + | Module _ -> failwith "Flags. not a list option (Module)" ;; let list_to_value c2v l = @@ -458,7 +458,7 @@ let from_value cl = cl.from_value;; let value_to_sum l v = match v with StringValue s -> List.assoc s l - | _ -> failwith "Options: not a sum option" + | _ -> failwith "Flags. not a sum option" ;; let sum_to_value l v = StringValue (List.assq v l);; @@ -659,8 +659,8 @@ let value_to_tuple2 (c1, c2) v = | List l | SmallList l -> Printf.printf "list of %d" (List.length l); print_newline (); - failwith "Options: not a tuple2 list option" - | _ -> failwith "Options: not a tuple2 option" + failwith "Flags. not a tuple2 list option" + | _ -> failwith "Flags. not a tuple2 option" ;; let tuple2_option p = @@ -675,7 +675,7 @@ let value_to_tuple3 (c1, c2, c3) v = List [v1; v2; v3] -> from_value c1 v1, from_value c2 v2, from_value c3 v3 | SmallList [v1; v2; v3] -> from_value c1 v1, from_value c2 v2, from_value c3 v3 - | _ -> failwith "Options: not a tuple3 option" + | _ -> failwith "Flags. not a tuple3 option" ;; let tuple3_option p = @@ -691,7 +691,7 @@ let value_to_tuple4 (c1, c2, c3, c4) v = (from_value c1 v1, from_value c2 v2, from_value c3 v3, from_value c4 v4) | SmallList [v1; v2; v3; v4] -> (from_value c1 v1, from_value c2 v2, from_value c3 v3, from_value c4 v4) - | _ -> failwith "Options: not a tuple4 option" + | _ -> failwith "Flags. not a tuple4 option" ;; let tuple4_option p = -- cgit v1.2.3