summaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /ide
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'ide')
-rw-r--r--ide/command_windows.ml50
-rw-r--r--ide/command_windows.mli6
-rw-r--r--ide/coq.ml511
-rw-r--r--ide/coq.mli56
-rw-r--r--ide/coq.pngbin9101 -> 5821 bytes
-rw-r--r--ide/coq_commands.ml11
-rw-r--r--ide/coqide.ml695
-rw-r--r--ide/highlight.mll141
-rw-r--r--ide/ideutils.ml121
-rw-r--r--ide/ideutils.mli8
-rw-r--r--ide/index_urls.txt563
-rw-r--r--ide/preferences.ml121
-rw-r--r--ide/preferences.mli11
-rw-r--r--ide/utf8.v56
-rw-r--r--ide/utils/config_file.ml4
-rw-r--r--ide/utils/configwin_ihm.ml12
-rw-r--r--ide/utils/uoptions.ml32
17 files changed, 1170 insertions, 1228 deletions
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 "<date not printable>" 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
--- a/ide/coq.png
+++ b/ide/coq.png
Binary files 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 *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,25 +7,32 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coqide.ml 10229 2007-10-16 18:44:54Z notin $ *)
+(* $Id: coqide.ml 11126 2008-06-13 18:45:04Z herbelin $ *)
open Preferences
open Vernacexpr
open Coq
open Ideutils
-let out_some s = match s with
- | None -> 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
@@ -2086,6 +2140,9 @@ let main files =
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 "<Proof _Wizard>"
~key:GdkKeysyms._dollar
~callback:(do_if_active (fun a -> a#tactic_wizard
@@ -2831,6 +2891,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
())
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
(Command_windows.command_window ())#new_command
@@ -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:"<CoqIde MenuBar>/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:"<CoqIde MenuBar>/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:"<CoqIde MenuBar>/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:"<CoqIde MenuBar>/Windows" ~accel_group
+ let configuration_factory = new GMenu.factory configuration_menu
+ ~accel_path:"<CoqIde MenuBar>/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_equal<I>i</I>,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 *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Logic *)
-Notation "∀ x , P" :=
- (forall x , P) (at level 200, x ident) : type_scope.
-Notation "∀ x y , P" :=
- (forall x y , P) (at level 200, x ident, y ident) : type_scope.
-Notation "∀ x y z , P" :=
- (forall x y z , P) (at level 200, x ident, y ident, z ident) : type_scope.
-Notation "∀ x y z u , P" :=
- (forall x y z u , P) (at level 200, x ident, y ident, z ident, u ident) : type_scope.
-Notation "∀ x : t , P" :=
- (forall x : t , P) (at level 200, x ident) : type_scope.
-Notation "∀ x y : t , P" :=
- (forall x y : t , P) (at level 200, x ident, y ident) : type_scope.
-Notation "∀ x y z : t , P" :=
- (forall x y z : t , P) (at level 200, x ident, y ident, z ident) : type_scope.
-Notation "∀ x y z u : t , P" :=
- (forall x y z u : t , P) (at level 200, x ident, y ident, z ident, u ident) : type_scope.
-
-Notation "∃ x , P" := (exists x , P) (at level 200, x ident) : type_scope.
-Notation "∃ x : t , P" := (exists x : t, P) (at level 200, x ident) : type_scope.
-
-Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope.
-Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope.
-Notation "x → y" := (x -> 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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 16:19:57 +0000