From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- ide/coq.ico | Bin 27574 -> 0 bytes ide/coq.ml | 13 ++++++------- ide/coqide.ml | 30 ++++++++++++++++-------------- ide/highlight.mll | 19 +++++++++++-------- ide/ideutils.ml | 7 ++----- ide/undo_lablgtk_ge212.mli | 36 ++++++++++++++++++++++++++++++++++++ 6 files changed, 71 insertions(+), 34 deletions(-) delete mode 100644 ide/coq.ico create mode 100644 ide/undo_lablgtk_ge212.mli (limited to 'ide') diff --git a/ide/coq.ico b/ide/coq.ico deleted file mode 100644 index b99f6399..00000000 Binary files a/ide/coq.ico and /dev/null differ diff --git a/ide/coq.ml b/ide/coq.ml index c560f0db..e2649c82 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 11238 2008-07-19 09:34:03Z herbelin $ *) +(* $Id: coq.ml 11826 2009-01-22 06:43:35Z notin $ *) open Vernac open Vernacexpr @@ -58,7 +58,7 @@ let get_version_date () = then Coq_config.date else "" in try - let ch = open_in (Coq_config.coqtop^"/revision") in + let ch = open_in (Coq_config.coqsrc^"/revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -79,7 +79,7 @@ let version () = 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") + (if Mltop.is_native then "native" else "bytecode") (if Coq_config.best="opt" then "native" else "bytecode") let is_in_coq_lib dir = @@ -88,7 +88,7 @@ let is_in_coq_lib dir = List.exists (fun s -> let fdir = - Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in + Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in prerr_endline (" Comparing to: "^fdir); if is_same_file fdir then (prerr_endline " YES";true) else (prerr_endline"NO";false)) @@ -230,7 +230,6 @@ let rec attribute_of_vernac_command = function (* Gallina extensions *) | VernacBeginSection _ -> [] | VernacEndSegment _ -> [] - | VernacRecord _ -> [] | VernacRequire _ -> [] | VernacImport _ -> [] | VernacCanonical _ -> [] @@ -238,7 +237,6 @@ let rec attribute_of_vernac_command = function | VernacIdentityCoercion _ -> [] (* Type classes *) - | VernacClass _ -> [] | VernacInstance _ -> [] | VernacContext _ -> [] | VernacDeclareInstance _ -> [] @@ -273,6 +271,7 @@ let rec attribute_of_vernac_command = function (* Commands *) | VernacDeclareTacticDefinition _ -> [] + | VernacCreateHintDb _ -> [] | VernacHints _ -> [] | VernacSyntacticDefinition _ -> [] | VernacDeclareImplicits _ -> [] @@ -386,7 +385,7 @@ let compute_reset_info = function | VernacDefinition (_, (_,id), DefineBody _, _) | VernacAssumption (_,_ ,(_,((_,id)::_,_))::_) - | VernacInductive (_, (((_,id),_,_,_),_) :: _) -> + | VernacInductive (_, (((_,(_,id)),_,_,_,_),_) :: _) -> ResetAtRegisteredObject (reset_mark id), undo_info(), ref true | com when is_vernac_proof_ending_command com -> NoReset, undo_info(), ref true diff --git a/ide/coqide.ml b/ide/coqide.ml index 07ee698f..ea2dfe4d 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 11221 2008-07-11 23:28:25Z herbelin $ *) +(* $Id: coqide.ml 11853 2009-01-23 18:40:58Z notin $ *) open Preferences open Vernacexpr @@ -482,10 +482,11 @@ let input_channel b ic = Buffer.add_substring b buf 0 !len done -let with_file name ~f = - let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in - try f ic; close_in ic with exn -> - close_in ic; !flash_info ("Error: "^Printexc.to_string exn) +let with_file handler name ~f = + try + let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in + try f ic; close_in ic with e -> close_in ic; raise e + with Sys_error s -> handler s type info = {start:GText.mark; stop:GText.mark; @@ -713,7 +714,7 @@ object(self) try if is_active then self#reset_initial; let b = Buffer.create 1024 in - with_file f ~f:(input_channel b); + with_file !flash_info f ~f:(input_channel b); let s = try_convert (Buffer.contents b) in input_buffer#set_text s; self#update_stats; @@ -1839,7 +1840,7 @@ let main files = ~title:"CoqIde" () in (try - let icon_image = lib_ide_file "coq.ico" in + let icon_image = lib_ide_file "coq.png" in let icon = GdkPixbuf.from_file icon_image in w#set_icon (Some icon) with _ -> ()); @@ -1871,7 +1872,7 @@ let main files = let file_factory = new GMenu.factory ~accel_path:"/File/" file_menu ~accel_group in (* File/Load Menu *) - let load f = + let load_file handler f = let f = absolute_filename f in try prerr_endline "Loading file starts"; @@ -1886,7 +1887,7 @@ let main files = prerr_endline "Loading: must open"; let b = Buffer.create 1024 in prerr_endline "Loading: get raw content"; - with_file f ~f:(input_channel b); + with_file handler f ~f:(input_channel b); prerr_endline "Loading: convert content"; let s = do_convert (Buffer.contents b) in prerr_endline "Loading: create view"; @@ -1922,8 +1923,9 @@ let main files = prerr_endline "Loading: success" with | Vector.Found i -> set_current_view i - | e -> !flash_info ("Load failed: "^(Printexc.to_string e)) + | e -> handler ("Load failed: "^(Printexc.to_string e)) in + let load f = load_file !flash_info f in let load_m = file_factory#add_item "_New" ~key:GdkKeysyms._N in let load_f () = @@ -2478,7 +2480,7 @@ let main files = (fun () -> let av = Option.get ((get_current_view()).analyzed_view) in match av#filename with - | None -> () + | None -> warning "Call to external editor available only on named files" | Some f -> save_f (); let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in @@ -3632,9 +3634,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); begin List.iter (fun f -> if Sys.file_exists f then load f else - if Filename.check_suffix f ".v" - then load f - else load (f^".v")) files; + let f = if Filename.check_suffix f ".v" then f else f^".v" in + load_file (fun s -> print_endline s; exit 1) f) + files; activate_input 0 end else diff --git a/ide/highlight.mll b/ide/highlight.mll index 8cd55c97..f2ecaa9c 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: highlight.mll 11004 2008-05-28 09:09:12Z herbelin $ *) +(* $Id: highlight.mll 11481 2008-10-20 19:23:51Z herbelin $ *) { @@ -110,13 +110,16 @@ rule next_starting_order = parse | 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 + { if id = "Time" then next_starting_order lexbuf else + begin + 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 + end } | _ { starting := false; next_interior_order lexbuf} | eof { raise End_of_file } diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d851dc2f..d9b5e572 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 11093 2008-06-10 18:41:33Z barras $ *) +(* $Id: ideutils.ml 11749 2009-01-05 14:01:04Z notin $ *) open Preferences @@ -33,10 +33,7 @@ let prerr_string s = if !debug then (prerr_string s;flush stderr) let lib_ide_file f = - let coqlib = - System.getenv_else "COQLIB" - (if Coq_config.local || !Flags.boot then Coq_config.coqtop - else Coq_config.coqlib) in + let coqlib = Envars.coqlib () in Filename.concat (Filename.concat coqlib "ide") f let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli new file mode 100644 index 00000000..916a06e9 --- /dev/null +++ b/ide/undo_lablgtk_ge212.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Gtk.text_view] Gtk.obj -> +object + inherit GText.view + method undo : bool + method redo : bool + method clear_undo : unit +end + +val undoable_view : + ?buffer:GText.buffer -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?accepts_tab:bool -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + undoable_view + + -- cgit v1.2.3