diff options
author | 2011-12-25 13:19:42 +0100 | |
---|---|---|
committer | 2011-12-25 13:19:42 +0100 | |
commit | 300293c119981054c95182a90c829058530a6b6f (patch) | |
tree | d7303613741c5796b58ced7db24ec7203327dbb2 /ide | |
parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) |
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'ide')
-rw-r--r-- | ide/command_windows.ml | 4 | ||||
-rw-r--r-- | ide/command_windows.mli | 4 | ||||
-rw-r--r-- | ide/config_lexer.mll | 4 | ||||
-rw-r--r-- | ide/config_parser.mly | 4 | ||||
-rw-r--r-- | ide/coq.ml | 6 | ||||
-rw-r--r-- | ide/coq.mli | 4 | ||||
-rw-r--r-- | ide/coq_commands.ml | 4 | ||||
-rw-r--r-- | ide/coq_lex.mll | 4 | ||||
-rw-r--r-- | ide/coq_tactics.ml | 4 | ||||
-rw-r--r-- | ide/coq_tactics.mli | 4 | ||||
-rw-r--r-- | ide/coqide.ml | 78 | ||||
-rw-r--r-- | ide/coqide.mli | 4 | ||||
-rw-r--r-- | ide/gtk_parsing.ml | 2 | ||||
-rw-r--r-- | ide/highlight.mll | 4 | ||||
-rw-r--r-- | ide/ideutils.ml | 4 | ||||
-rw-r--r-- | ide/ideutils.mli | 4 | ||||
-rw-r--r-- | ide/preferences.ml | 4 | ||||
-rw-r--r-- | ide/preferences.mli | 4 | ||||
-rw-r--r-- | ide/tags.ml | 2 | ||||
-rw-r--r-- | ide/typed_notebook.ml | 2 | ||||
-rw-r--r-- | ide/uim/coqide-rules.scm | 2 | ||||
-rw-r--r-- | ide/undo.ml | 4 | ||||
-rw-r--r-- | ide/undo_lablgtk_ge212.mli | 2 | ||||
-rw-r--r-- | ide/undo_lablgtk_ge26.mli | 4 | ||||
-rw-r--r-- | ide/undo_lablgtk_lt26.mli | 4 | ||||
-rw-r--r-- | ide/utf8_convert.mll | 4 |
26 files changed, 91 insertions, 79 deletions
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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command_windows.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: command_windows.ml 14641 2011-11-06 11:59:10Z herbelin $ *) class command_window () = (* let window = GWindow.window diff --git a/ide/command_windows.mli b/ide/command_windows.mli index eb0aa568..0f5c208b 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command_windows.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: command_windows.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) class command_window : unit -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: config_lexer.mll 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: config_lexer.mll 14641 2011-11-06 11:59:10Z herbelin $ *) { diff --git a/ide/config_parser.mly b/ide/config_parser.mly index 0859cbe0..d49e22eb 100644 --- a/ide/config_parser.mly +++ b/ide/config_parser.mly @@ -1,12 +1,12 @@ /************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************/ -/* $Id: config_parser.mly 13323 2010-07-24 15:57:30Z herbelin $ */ +/* $Id: config_parser.mly 14641 2011-11-06 11:59:10Z herbelin $ */ %{ @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 13751 2010-12-24 09:56:05Z letouzey $ *) +(* $Id: coq.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Vernac open Vernacexpr @@ -297,7 +297,7 @@ let rec attribute_of_vernac_command = function (* Proof management *) | VernacGoal _ -> [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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: coq.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names open Term diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index c8a5c940..d41bcf29 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_commands.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coq_commands.ml 14641 2011-11-06 11:59:10Z herbelin $ *) let commands = [ [(* "Abort"; *) diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index 5bff10b3..02e21166 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -67,7 +67,7 @@ let is_proof_end = let h = Hashtbl.create 97 in List.iter (fun s -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coq_tactics.ml 14641 2011-11-06 11:59:10Z herbelin $ *) let tactics = [ "Abstract"; diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli index e33c73ab..4c583d3a 100644 --- a/ide/coq_tactics.mli +++ b/ide/coq_tactics.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq_tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: coq_tactics.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) val tactics : string list diff --git a/ide/coqide.ml b/ide/coqide.ml index ce4f0666..162728ad 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 13751 2010-12-24 09:56:05Z letouzey $ *) +(* $Id: coqide.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Preferences open Vernacexpr @@ -306,7 +306,8 @@ let remove_current_view_page () = kill_input_view c in let current = session_notebook#current_term in - if current.script#buffer#modified then + if not current.script#buffer#modified then do_remove () + else match GToolbox.question_box ~title:"Close" ~buttons:["Save Buffer and Close"; "Close without Saving"; @@ -1680,34 +1681,42 @@ let choose_save session = save_dialog#show () *) +(* Nota: using && here has the advantage of working both under win32 and unix. + If someday we want the main command to be tried even if the "cd" has failed, + then we should use " ; " under unix but " & " under win32 (cf. #2363). +*) + +let local_cd file = + "cd " ^ Filename.quote (Filename.dirname file) ^ " && " + let do_print session = let av = session.analyzed_view in - if session.filename = "" - then flash_info "Cannot print: this buffer has no name" - else begin - let cmd = - "cd " ^ Filename.quote (Filename.dirname session.filename) ^ "; " ^ - !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^ - " | " ^ !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 - + match av#filename with + |None -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqide.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: coqide.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* The CoqIde main module. The following function [start] will parse the command line, initialize the load path, load the input diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index ddf4a754..1b52dba3 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/highlight.mll b/ide/highlight.mll index dfcc4354..c288d6a3 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: highlight.mll 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: highlight.mll 14641 2011-11-06 11:59:10Z herbelin $ *) { diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8b7840e3..a6be77f2 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 13751 2010-12-24 09:56:05Z letouzey $ *) +(* $Id: ideutils.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Preferences diff --git a/ide/ideutils.mli b/ide/ideutils.mli index ade460c6..d6311c78 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ideutils.mli 13751 2010-12-24 09:56:05Z letouzey $ i*) +(*i $Id: ideutils.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) val async : ('a -> 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 *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 13436 2010-09-19 10:18:18Z herbelin $ *) +(* $Id: preferences.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Configwin open Printf diff --git a/ide/preferences.mli b/ide/preferences.mli index 50659717..472ae30f 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: preferences.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: preferences.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) type pref = { diff --git a/ide/tags.ml b/ide/tags.ml index f6ffcde4..aacac46e 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml index e674212c..3dd2279f 100644 --- a/ide/typed_notebook.ml +++ b/ide/typed_notebook.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/uim/coqide-rules.scm b/ide/uim/coqide-rules.scm index c483c88b..af25b613 100644 --- a/ide/uim/coqide-rules.scm +++ b/ide/uim/coqide-rules.scm @@ -1,6 +1,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; v ; The Coq Proof Assistant / The Coq Development Team ;; -;; <O___,, ; INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 ;; +;; <O___,, ; INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 ;; ;; \VV/ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; // ; This file is distributed under the terms of the ;; ;; ; GNU Lesser General Public License Version 2.1 ;; diff --git a/ide/undo.ml b/ide/undo.ml index 819b4807..55d0f288 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: undo.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: undo.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open GText open Ideutils diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli index 6cc4757b..1326a486 100644 --- a/ide/undo_lablgtk_ge212.mli +++ b/ide/undo_lablgtk_ge212.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli index c260f171..698b34c5 100644 --- a/ide/undo_lablgtk_ge26.mli +++ b/ide/undo_lablgtk_ge26.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: undo_lablgtk_ge26.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: undo_lablgtk_ge26.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* An undoable view class *) diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli index c9d1bacb..e99d3141 100644 --- a/ide/undo_lablgtk_lt26.mli +++ b/ide/undo_lablgtk_lt26.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: undo_lablgtk_lt26.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: undo_lablgtk_lt26.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* An undoable view class *) diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll index 5034ab3c..ce0c4836 100644 --- a/ide/utf8_convert.mll +++ b/ide/utf8_convert.mll @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: utf8_convert.mll 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: utf8_convert.mll 14641 2011-11-06 11:59:10Z herbelin $ *) { open Lexing |