diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 254 | ||||
| -rw-r--r-- | ide/coq.mli | 8 | ||||
| -rw-r--r-- | ide/coqide.ml | 77 | ||||
| -rw-r--r-- | ide/ideutils.ml | 11 | ||||
| -rw-r--r-- | ide/index_urls.txt | 563 | ||||
| -rw-r--r-- | ide/preferences.ml | 53 | ||||
| -rw-r--r-- | ide/preferences.mli | 4 |
7 files changed, 269 insertions, 701 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index e75f507210..aef993be65 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -110,6 +110,166 @@ let is_in_proof_mode () = let user_error_loc l s = raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) +type command_attribute = + NavigationCommand | QueryCommand | DebugCommand + | OtherStatePreservingCommand | GoalStartingCommand + +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 _ -> [] + | VernacExactProof _ -> [] + + | 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 _ -> [] + | VernacSolveExistential _ -> [] + + (* 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 _ -> [] + | VernacUnsetOption _ -> [] + | 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 _ -> [] + | VernacUnfocus -> [] + | VernacGo _ -> [] + | VernacShow _ -> [OtherStatePreservingCommand] + | VernacCheckGuard -> [OtherStatePreservingCommand] + | VernacProof (Tacexpr.TacId []) -> [OtherStatePreservingCommand] + | VernacProof _ -> [] + + (* Toplevel control *) + | VernacToplevelControl _ -> [] + + (* Extensions *) + | 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_debug_command com = + List.mem DebugCommand (attribute_of_vernac_command com) + +let is_vernac_state_preserving_command com = + let attribute = attribute_of_vernac_command com in + let b = + List.mem OtherStatePreservingCommand attribute or + List.mem QueryCommand attribute in + if b then prerr_endline "state preserving command found"; + b + +let rec is_tactic = function + | VernacSolve _ -> true + | VernacTime com -> is_tactic com + | _ -> false + let interp verbosely s = prerr_endline "Starting interp..."; prerr_endline s; @@ -118,51 +278,20 @@ 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 _ - | VernacExtend("Extraction", _) - | VernacExtend("ExtractionLibrary",_) - | VernacExtend("RecursiveExtractionLibrary",_) - -> Flags.make_silent (not verbosely) - | _ -> () - end; - Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); - Flags.make_silent true; - prerr_endline ("...Done with interp of : "^s); - last + if is_vernac_goal_starting_command vernac & is_in_proof_mode () then + user_error_loc loc (str "CoqIDE do not support nested goals"); + 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_query_command vernac then + !flash_info + "Warning: query commands should not be inserted in scripts"; + Flags.make_silent (not verbosely); (*verbose if in small step forward*) + Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); + Flags.make_silent true; + prerr_endline ("...Done with interp of : "^s); + last let interp_and_replace s = let result = interp false s in @@ -199,11 +328,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 @@ -339,20 +463,24 @@ let word_class s = SHashtbl.find word_tbl s with Not_found -> Normal -type reset_info = NoReset | Reset of Names.identifier * bool ref +type reset_info = + | NoReset + | ResetAtDecl of Names.identifier * bool ref + | ResetAtSegmentStart of Names.identifier * bool ref let compute_reset_info = function - | VernacDefinition (_, (_,id), DefineBody _, _) - | VernacBeginSection (_,id) - | VernacDefineModule (_,(_,id), _, _, _) - | VernacDeclareModule (_,(_,id), _, _) - | VernacDeclareModuleType ((_,id), _, _) + | VernacBeginSection id + | VernacDefineModule (_,id, _, _, _) + | VernacDeclareModule (_,id, _, _) + | VernacDeclareModuleType (id, _, _) -> + ResetAtSegmentStart (snd id, ref true) + | VernacDefinition (_, (_,id), DefineBody _, _) | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> - Reset (id, ref true) + ResetAtDecl (id, ref true) | VernacDefinition (_, (_,id), ProveBody _, _) | VernacStartTheoremProof (_, [Some (_,id), _], _, _) -> - Reset (id, ref false) + ResetAtDecl (id, ref false) | _ -> NoReset let reset_initial () = @@ -472,16 +600,6 @@ 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 diff --git a/ide/coq.mli b/ide/coq.mli index 991f104dbe..32a62c2306 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -21,7 +21,8 @@ val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string val is_tactic : Vernacexpr.vernac_expr -> bool -val is_state_preserving : Vernacexpr.vernac_expr -> bool +val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool +val is_vernac_goal_starting_command : Vernacexpr.vernac_expr -> bool (* type hyp = (identifier * constr option * constr) * string *) @@ -41,7 +42,10 @@ val print_no_goal : unit -> string val process_exn : exn -> string*(Util.loc option) -type reset_info = NoReset | Reset of Names.identifier * bool ref +type reset_info = + | NoReset + | ResetAtDecl of Names.identifier * bool ref + | ResetAtSegmentStart of Names.identifier * bool ref val compute_reset_info : Vernacexpr.vernac_expr -> reset_info val reset_initial : unit -> unit diff --git a/ide/coqide.ml b/ide/coqide.ml index f223972df6..29b55da6aa 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -459,7 +459,7 @@ let rec complete input_buffer w (offset:int) = let get_current_word () = let av = Option.get ((get_current_view ()).analyzed_view) in - match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with + match (cb ())#text with | None -> prerr_endline "None selected"; let it = av#get_insert in @@ -498,19 +498,16 @@ 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 update_on_end_of_proof () = let lookup_lemma = function - | { ast = _, ( VernacDefinition (_, _, ProveBody _, _) - | VernacDeclareTacticDefinition _ - | VernacStartTheoremProof _) ; - reset_info = Reset (_, r) } -> - if not !r then begin + | { reset_info = ResetAtDecl (_, r) } -> + if not !r then begin prerr_endline "Toggling Reset info to true"; r := true; raise Exit end else begin + (* Hide the Definition done since last started proof *) prerr_endline "Toggling Changing Reset id"; r := false end @@ -521,13 +518,9 @@ let update_on_end_of_proof id = 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', r) } when id = id' -> raise Exit + | { reset_info = ResetAtSegmentStart (_, r) } -> r := false + | { reset_info = ResetAtDecl (_, r) } -> r := false | _ -> () in try Stack.iter lookup_section processed_stack with Exit -> () @@ -537,21 +530,26 @@ let push_phrase start_of_phrase_mark end_of_phrase_mark ast = stop = end_of_phrase_mark; ast = ast; reset_info = Coq.compute_reset_info (snd ast) - } - in - push x; + } in + begin match snd ast with | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () - | VernacEndSegment id -> update_on_end_of_segment id + | VernacEndSegment (_,id) -> 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; + begin match snd x.ast with | VernacEndProof (Proved (_, None)) -> update_on_end_of_proof () - | VernacEndSegment id -> update_on_end_of_segment id + | VernacEndSegment (_,id) -> update_on_end_of_segment id | _ -> () + end; + push x + (* For electric handlers *) exception Found @@ -1284,13 +1282,10 @@ object(self) 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) + | ResetAtSegmentStart (id, ({contents=true} as v)) -> + v:=false; reset_to_mod id + | ResetAtDecl (id, ({contents=true} as v)) -> + v:=false; reset_to id | _ -> synchro () end; interp_last t.ast; @@ -1388,20 +1383,16 @@ Please restart and report NOW."; 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})} -> + + | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> + ignore (pop ()); + reset_to_mod id; + sync update_input () + | {reset_info=ResetAtDecl (id, {contents=true})} -> ignore (pop ()); - (match t with - | VernacBeginSection _ | VernacDefineModule _ - | VernacDeclareModule _ | VernacDeclareModuleType _ - | VernacEndSegment _ - -> reset_to_mod id - | _ -> reset_to id); + reset_to id; sync update_input () - | { ast = _, ( VernacStartTheoremProof _ - | VernacGoal _ - | VernacDeclareTacticDefinition _ - | VernacDefinition (_,_,ProveBody _,_)); - reset_info=Reset(id,{contents=false})} -> + | {reset_info=ResetAtDecl (id,{contents=false})} -> ignore (pop ()); (try Pfedit.delete_current_proof () @@ -1411,7 +1402,7 @@ Please restart and report NOW."; raise e end); sync update_input () - | { ast = (_, a) } when is_state_preserving a -> + | { ast = (_, a) } when is_vernac_state_preserving_command a -> ignore (pop ()); sync update_input () | _ -> @@ -2418,8 +2409,8 @@ let main files = | 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 diff --git a/ide/ideutils.ml b/ide/ideutils.ml index b79e4b9361..f4fd73d6fd 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -268,9 +268,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,_res) = run_command f com in + if s = Unix.WEXITED 127 then + prerr_endline + ("Could not execute\n \""^com^"\"\ncheck your preferences for setting a valid browser command") let url_for_keyword = let ht = Hashtbl.create 97 in @@ -295,7 +297,8 @@ 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 -> + prerr_endline ("No documentation found for "^text) let underscore = Glib.Utf8.to_unichar "_" (ref 0) diff --git a/ide/index_urls.txt b/ide/index_urls.txt deleted file mode 100644 index fea61809df..0000000000 --- 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 31edcdd1b7..aeaeb4ec17 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -75,8 +75,8 @@ type pref = mutable modifier_for_tactics : 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; @@ -128,10 +128,7 @@ let (current:pref ref) = cmd_browse = Flags.browser_cmd_fmt; - cmd_editor = - if Sys.os_type = "Win32" - then "NOTEPAD ", "" - else "emacs ", ""; + 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 "Monospace 10"; @@ -199,8 +196,8 @@ let save_pref () = (List.map mod_to_str p.modifier_for_tactics) ++ 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] ++ @@ -233,6 +230,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); @@ -257,8 +257,8 @@ let load_pref () = (fun v -> np.modifier_for_tactics <- 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); @@ -480,20 +480,35 @@ let configure ?(apply=(fun () -> ())) () = ~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 diff --git a/ide/preferences.mli b/ide/preferences.mli index 9d85b51085..9251730ff2 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -34,8 +34,8 @@ type pref = mutable modifier_for_tactics : 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; |