From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- ide/command_windows.ml | 4 +-- ide/command_windows.mli | 4 +-- ide/config_lexer.mll | 4 +-- ide/config_parser.mly | 4 +-- ide/coq.ml | 6 ++-- ide/coq.mli | 4 +-- ide/coq_commands.ml | 4 +-- ide/coq_lex.mll | 4 +-- ide/coq_tactics.ml | 4 +-- ide/coq_tactics.mli | 4 +-- ide/coqide.ml | 78 ++++++++++++++++++++++++++-------------------- ide/coqide.mli | 4 +-- ide/gtk_parsing.ml | 2 +- ide/highlight.mll | 4 +-- ide/ideutils.ml | 4 +-- ide/ideutils.mli | 4 +-- ide/preferences.ml | 4 +-- ide/preferences.mli | 4 +-- ide/tags.ml | 2 +- ide/typed_notebook.ml | 2 +- ide/uim/coqide-rules.scm | 2 +- ide/undo.ml | 4 +-- ide/undo_lablgtk_ge212.mli | 2 +- ide/undo_lablgtk_ge26.mli | 4 +-- ide/undo_lablgtk_lt26.mli | 4 +-- ide/utf8_convert.mll | 4 +-- 26 files changed, 91 insertions(+), 79 deletions(-) (limited to 'ide') diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 4510189b..1df83803 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 4e3ffd89..3724f2bf 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* [GoalStartingCommand] - | VernacAbort _ -> [NavigationCommand] + | VernacAbort _ -> [] | VernacAbortAll -> [NavigationCommand] | VernacRestart -> [NavigationCommand] | VernacSuspend -> [NavigationCommand] diff --git a/ide/coq.mli b/ide/coq.mli index af17c0e9..9dec52c6 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Hashtbl.add h s ()) - [ "Qed" ; "Defined" ; "Admitted" ]; + [ "Qed" ; "Defined" ; "Admitted"; "Abort" ]; Hashtbl.mem h let start = ref true diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml index e3d8131e..568594bd 100644 --- a/ide/coq_tactics.ml +++ b/ide/coq_tactics.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* flash_info "Cannot print: this buffer has no name" + |Some f_name -> begin + let cmd = + local_cd session.filename ^ + !current.cmd_coqdoc ^ " --coqlib_path " ^ Envars.coqlib () ^ + " -ps " ^ Filename.quote (Filename.basename f_name) ^ + " | " ^ !current.cmd_print + in + let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () 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 () + end let main files = (* Statup preferences *) @@ -1956,8 +1965,11 @@ let main files = | _ -> assert false in let cmd = - "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ - !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) + local_cd f ^ + !current.cmd_coqdoc ^ " --coqlib_path " ^ + Envars.coqlib () ^ " --" ^ kind ^ + " -o " ^ (Filename.quote output) ^ " " ^ + (Filename.quote basef) in let s,_ = run_command av#insert_message cmd in flash_info (cmd ^ @@ -2862,7 +2874,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); flash_info "Cannot make: this buffer has no name" | Some f -> let cmd = - "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in + local_cd f ^ !current.cmd_make in (* save_f (); @@ -2929,7 +2941,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); flash_info "Cannot make makefile: this buffer has no name" | Some f -> let cmd = - "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in + local_cd f ^ !current.cmd_coqmakefile in let s,res = run_command av#insert_message cmd in flash_info (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") diff --git a/ide/coqide.mli b/ide/coqide.mli index b70a9b4b..ea995c71 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* unit) -> 'a -> unit val sync : ('a -> 'b) -> 'a -> 'b diff --git a/ide/preferences.ml b/ide/preferences.ml index 5d97f659..790bf560 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*