From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- ide/blaster_window.ml | 178 -- ide/command_windows.ml | 66 +- ide/command_windows.mli | 2 +- ide/config_lexer.mll | 10 +- ide/config_parser.mly | 2 +- ide/coq.ml | 340 +-- ide/coq.mli | 40 +- ide/coq_commands.ml | 19 +- ide/coq_lex.mll | 194 ++ ide/coq_tactics.ml | 2 +- ide/coq_tactics.mli | 2 +- ide/coqide.ml | 4012 ++++++++++++++++-------------------- ide/coqide.mli | 4 +- ide/extract_index.mll | 31 - ide/find_phrase.mll | 74 - ide/gtk_parsing.ml | 176 ++ ide/highlight.mll | 92 +- ide/ide.mllib | 23 + ide/ideutils.ml | 180 +- ide/ideutils.mli | 20 +- ide/preferences.ml | 291 +-- ide/preferences.mli | 4 +- ide/tags.ml | 50 + ide/typed_notebook.ml | 68 + ide/uim/coqide-custom.scm | 105 + ide/uim/coqide-rules.scm | 1223 +++++++++++ ide/uim/coqide.scm | 277 +++ ide/undo.ml | 68 +- ide/undo_lablgtk_ge212.mli | 2 +- ide/undo_lablgtk_ge26.mli | 4 +- ide/undo_lablgtk_lt26.mli | 4 +- ide/utf8_convert.mll | 12 +- ide/utils/config_file.ml | 2 +- ide/utils/configwin.ml | 2 - ide/utils/configwin.mli | 16 +- ide/utils/configwin_html_config.ml | 84 - ide/utils/configwin_ihm.ml | 126 +- ide/utils/configwin_keys.ml | 50 +- ide/utils/configwin_types.ml | 10 +- ide/utils/editable_cells.ml | 92 +- ide/utils/okey.mli | 64 +- ide/utils/uoptions.ml | 772 ------- ide/utils/uoptions.mli | 148 -- 43 files changed, 4679 insertions(+), 4262 deletions(-) delete mode 100644 ide/blaster_window.ml create mode 100644 ide/coq_lex.mll delete mode 100644 ide/extract_index.mll delete mode 100644 ide/find_phrase.mll create mode 100644 ide/gtk_parsing.ml create mode 100644 ide/ide.mllib create mode 100644 ide/tags.ml create mode 100644 ide/typed_notebook.ml create mode 100644 ide/uim/coqide-custom.scm create mode 100644 ide/uim/coqide-rules.scm create mode 100644 ide/uim/coqide.scm delete mode 100644 ide/utils/configwin_html_config.ml delete mode 100644 ide/utils/uoptions.ml delete mode 100644 ide/utils/uoptions.mli (limited to 'ide') diff --git a/ide/blaster_window.ml b/ide/blaster_window.ml deleted file mode 100644 index f3cb1e60..00000000 --- a/ide/blaster_window.ml +++ /dev/null @@ -1,178 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Coq.tried_tactic) (on_click:unit -> unit) = - let root_iter = - try Hashtbl.find roots root - with Not_found -> - let nr = new_arg root in - Hashtbl.add roots root nr; - nr - in - let nt = new_tac root_iter name in - let old_val = try MyMap.find root tbl with Not_found -> MyMap.empty in - tbl <- MyMap.add root (MyMap.add name (nt,compute,on_click) old_val) tbl - - method clear () = - model#clear (); - tbl <- MyMap.empty; - Hashtbl.clear roots; - - method blaster () = - view#expand_all (); - try MyMap.iter - (fun root_name l -> - try - MyMap.iter - (fun name (nt,compute,on_click) -> - match compute () with - | Coq.Interrupted -> - prerr_endline "Interrupted"; - raise Stop - | Coq.Failed -> - prerr_endline "Failed"; - ignore (model#remove nt) - (* model#set ~row:nt ~column:status false; - model#set ~row:nt ~column:nb_goals "N/A" - *) - | Coq.Success n -> - prerr_endline "Success"; - model#set ~row:nt ~column:status true; - model#set ~row:nt ~column:nb_goals (string_of_int n); - if n= -1 then raise Done - ) - l - with Done -> ()) - tbl; - Condition.signal blaster_killed; - prerr_endline "End of blaster"; - with Stop -> - Condition.signal blaster_killed; - prerr_endline "End of blaster (stopped !)"; - - initializer - ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true)); - ignore (view#selection#connect#after#changed ~callback: - begin fun () -> - prerr_endline "selection changed"; - List.iter - (fun path ->let pt = GtkTree.TreePath.to_string path in - let it = model#get_iter path in - prerr_endline (string_of_bool (model#iter_is_valid it)); - let name = model#get - ~row:(if String.length pt >1 then begin - ignore (GtkTree.TreePath.up path); - model#get_iter path - end else it - ) - ~column:argument in - let tactic = model#get ~row:it ~column:tactic in - prerr_endline ("Got name: "^name); - let success = model#get ~row:it ~column:status in - if success then try - prerr_endline "Got success"; - let _,_,f = MyMap.find tactic (MyMap.find name tbl) in - f (); - (* window#misc#hide () *) - with _ -> () - ) - view#selection#get_selected_rows - end); - -(* needs lablgtk2 update ignore (view#connect#after#row_activated - (fun path vcol -> - prerr_endline "Activated"; - ); -*) -end - -let blaster_window = ref None - -let main n = blaster_window := Some (new blaster_window n) - -let present_blaster_window () = match !blaster_window with - | None -> failwith "No blaster window." - | Some c -> c#window#misc#show (* present*) (); c - - -let blaster_window () = match !blaster_window with - | None -> failwith "No blaster window." - | Some c -> c - - diff --git a/ide/command_windows.ml b/ide/command_windows.ml index b84b0943..ee07b3fb 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command_windows.ml 11042 2008-06-03 12:45:38Z jnarboux $ *) +(* $Id$ *) -class command_window () = -(* let window = GWindow.window - ~allow_grow:true ~allow_shrink:true +class command_window () = +(* let window = GWindow.window + ~allow_grow:true ~allow_shrink:true ~width:500 ~height:250 ~position:`CENTER ~title:"CoqIde queries" ~show:false () @@ -19,23 +19,23 @@ class command_window () = let _ = frame#misc#hide () in let _ = GtkData.AccelGroup.create () in let hbox = GPack.hbox ~homogeneous:false ~packing:frame#add () in - let toolbar = GButton.toolbar - ~orientation:`VERTICAL + let toolbar = GButton.toolbar + ~orientation:`VERTICAL ~style:`ICONS - ~tooltips:true - ~packing:(hbox#pack + ~tooltips:true + ~packing:(hbox#pack ~expand:false ~fill:false) () in - let notebook = GPack.notebook ~scrollable:true - ~packing:(hbox#pack + let notebook = GPack.notebook ~scrollable:true + ~packing:(hbox#pack ~expand:true ~fill:true - ) + ) () in - let _ = + let _ = toolbar#insert_button ~tooltip:"Hide Commands Pane" ~text:"Hide Pane" @@ -43,7 +43,7 @@ class command_window () = ~callback:frame#misc#hide () in - let new_page_menu = + let new_page_menu = toolbar#insert_button ~tooltip:"New Page" ~text:"New Page" @@ -51,7 +51,7 @@ class command_window () = () in - let _ = + let _ = toolbar#insert_button ~tooltip:"Delete Page" ~text:"Delete Page" @@ -65,10 +65,10 @@ object(self) val new_page_menu = new_page_menu val notebook = notebook - method frame = frame + method frame = frame method new_command ?command ?term () = let appendp x = ignore (notebook#append_page x) in - let frame = GBin.frame + let frame = GBin.frame ~shadow_type:`ETCHED_OUT ~packing:appendp () @@ -84,15 +84,15 @@ object(self) () in combo#disable_activate (); - let on_activate c () = - if List.mem combo#entry#text Coq_commands.state_preserving then c () - else prerr_endline "Not a state preserving command" + let on_activate c () = + if List.mem combo#entry#text Coq_commands.state_preserving then c () + else prerr_endline "Not a state preserving command" in let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in entry#misc#set_can_default true; let r_bin = - GBin.scrolled_window - ~vpolicy:`AUTOMATIC + GBin.scrolled_window + ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(vbox#pack ~fill:true ~expand:true) () in let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in @@ -101,13 +101,13 @@ object(self) result#set_editable false; let callback () = let com = combo#entry#text in - let phrase = + let phrase = if String.get com (String.length com - 1) = '.' - then com ^ " " else com ^ " " ^ entry#text ^" . " + then com ^ " " else com ^ " " ^ entry#text ^" . " in try ignore(Coq.interp false phrase); - result#buffer#set_text + result#buffer#set_text ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ()) with e -> let (s,loc) = Coq.process_exn e in @@ -117,16 +117,16 @@ object(self) ignore (combo#entry#connect#activate ~callback:(on_activate callback)); ignore (ok_b#connect#clicked ~callback:(on_activate callback)); - begin match command,term with + begin match command,term with | None,None -> () - | Some c, None -> + | Some c, None -> combo#entry#set_text c; - - | Some c, Some t -> + + | Some c, Some t -> combo#entry#set_text c; entry#set_text t - - | None , Some t -> + + | None , Some t -> entry#set_text t end; on_activate callback (); @@ -134,9 +134,9 @@ object(self) entry#misc#grab_default (); ignore (entry#connect#activate ~callback); ignore (combo#entry#connect#activate ~callback); - self#frame#misc#show () + self#frame#misc#show () - initializer + initializer ignore (new_page_menu#connect#clicked self#new_command); (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*) end @@ -145,6 +145,6 @@ let command_window = ref None let main () = command_window := Some (new command_window ()) -let command_window () = match !command_window with +let command_window () = match !command_window with | None -> failwith "No command window." | Some c -> c diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 212e5692..4104f086 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: command_windows.mli 11011 2008-05-28 16:22:11Z jnarboux $ i*) +(*i $Id$ i*) class command_window : unit -> diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 7722e99a..97aeb2f5 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: config_lexer.mll 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) { @@ -28,19 +28,19 @@ rule token = parse | '#' [^ '\n']* { token lexbuf } | ident { IDENT (lexeme lexbuf) } | '=' { EQUAL } - | '"' { Buffer.reset string_buffer; + | '"' { Buffer.reset string_buffer; Buffer.add_char string_buffer '"'; string lexbuf; let s = Buffer.contents string_buffer in STRING (Scanf.sscanf s "%S" (fun s -> s)) } | _ { let c = lexeme_start lexbuf in - eprintf ".coqiderc: invalid character (%d)\n@." c; + eprintf ".coqiderc: invalid character (%d)\n@." c; token lexbuf } | eof { EOF } and string = parse | '"' { Buffer.add_char string_buffer '"' } - | '\\' '"' | _ + | '\\' '"' | _ { Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf } | eof { eprintf ".coqiderc: unterminated string\n@." } @@ -60,7 +60,7 @@ and string = parse | [] -> () | s :: sl -> fprintf fmt "%S@ %a" s print_list sl in - Stringmap.iter + Stringmap.iter (fun k s -> fprintf fmt "@[%s = %a@]@\n" k print_list s) m; fprintf fmt "@."; close_out c diff --git a/ide/config_parser.mly b/ide/config_parser.mly index 80cba27b..bd5577db 100644 --- a/ide/config_parser.mly +++ b/ide/config_parser.mly @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************/ -/* $Id: config_parser.mly 5920 2004-07-16 20:01:26Z herbelin $ */ +/* $Id$ */ %{ diff --git a/ide/coq.ml b/ide/coq.ml index a44428c7..bd441cf1 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml 11948 2009-02-27 16:01:53Z glondu $ *) +(* $Id$ *) open Vernac open Vernacexpr @@ -24,22 +24,23 @@ open Hipattern open Tacmach open Reductionops open Termops +open Namegen open Ideutils let prerr_endline s = if !debug then prerr_endline s else () let output = ref (Format.formatter_of_out_channel stdout) -let msg m = +let msg m = let b = Buffer.create 103 in Pp.msg_with (Format.formatter_of_buffer b) m; Buffer.contents b -let msgnl m = +let msgnl m = (msg m)^"\n" -let init () = - (* To hide goal in lower window. +let init () = + (* To hide goal in lower window. Problem: should not hide "xx is assumed" messages *) (**) @@ -70,7 +71,7 @@ let short_version () = let version () = let (ver,date) = get_version_date () in - Printf.sprintf + Printf.sprintf "The Coq Proof Assistant, version %s (%s)\ \nArchitecture %s running %s operating system\ \nGtk version is %s\ @@ -79,14 +80,14 @@ 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.is_native then "native" else "bytecode") - (if Coq_config.best="opt" 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 = +let is_in_coq_lib dir = prerr_endline ("Is it a coq theory ? : "^dir); let is_same_file = same_file dir in - List.exists - (fun s -> + List.exists + (fun s -> let fdir = Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in prerr_endline (" Comparing to: "^fdir); @@ -97,19 +98,19 @@ let is_in_coq_lib dir = let is_in_loadpath dir = Library.is_in_load_paths (System.physical_path_of_string dir) -let is_in_coq_path f = - try +let is_in_coq_path f = + try let base = Filename.chop_extension (Filename.basename f) in let _ = Library.locate_qualified_library false - (Libnames.make_qualid Names.empty_dirpath + (Libnames.make_qualid Names.empty_dirpath (Names.id_of_string base)) in prerr_endline (f ^ " is in coq path"); true - with _ -> + with _ -> prerr_endline (f ^ " is NOT in coq path"); - false + false -let is_in_proof_mode () = +let is_in_proof_mode () = match Decl_mode.get_current_mode () with Decl_mode.Mode_none -> false | _ -> true @@ -156,10 +157,7 @@ let prepare_option (l,dft) = 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 coqide_known_option table = List.mem table !known_options let with_printing_implicit = prepare_option printing_implicit_data let with_printing_coercions = prepare_option printing_coercions_data @@ -194,6 +192,8 @@ type command_attribute = let rec attribute_of_vernac_command = function (* Control *) | VernacTime com -> attribute_of_vernac_command com + | VernacTimeout(_,com) -> attribute_of_vernac_command com + | VernacFail com -> attribute_of_vernac_command com | VernacList _ -> [] (* unsupported *) | VernacLoad _ -> [] @@ -240,6 +240,7 @@ let rec attribute_of_vernac_command = function | VernacInstance _ -> [] | VernacContext _ -> [] | VernacDeclareInstance _ -> [] + | VernacDeclareClass _ -> [] (* Solving *) | VernacSolve _ -> [SolveCommand] @@ -275,11 +276,12 @@ let rec attribute_of_vernac_command = function | VernacHints _ -> [] | VernacSyntacticDefinition _ -> [] | VernacDeclareImplicits _ -> [] + | VernacDeclareReduction _ -> [] | VernacReserve _ -> [] + | VernacGeneralizable _ -> [] | VernacSetOpacity _ -> [] - | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> - [DebugCommand] - | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> + | VernacSetOption (_,["Ltac";"Debug"], _) -> [DebugCommand] + | VernacSetOption (_,o,BoolValue true) | VernacUnsetOption (_,o) -> if coqide_known_option o then [KnownOptionCommand] else [] | VernacSetOption _ -> [] | VernacRemoveOption _ -> [] @@ -358,75 +360,60 @@ 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_mark = Libnames.object_name 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 +type reset_info = { + status : reset_status; + proofs : identifier list; + cur_prf : (identifier * int) option; + loc_ast : Util.loc * Vernacexpr.vernac_expr; +} - | 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 compute_reset_info loc_ast = + let status,cur_prf = match snd loc_ast with + | com when is_vernac_proof_ending_command com -> NoReset,None + | VernacEndSegment _ -> NoReset,None + | com when is_vernac_tactic_command com -> + NoReset,Some (Pfedit.get_current_proof_name (), Pfedit.current_proof_depth ()) + | _ -> + (match Lib.has_top_frozen_state () with + | Some sp -> + prerr_endline ("On top of state "^Libnames.string_of_path (fst sp)); + ResetAtRegisteredObject sp,None + | None -> NoReset,None) + in + { status = status; + proofs = Pfedit.get_all_proof_names (); + cur_prf = cur_prf; + loc_ast = loc_ast; + } -let reset_initial () = +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 -> +let reset_to 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 = +let interp_with_options verbosely options s = prerr_endline "Starting interp..."; prerr_endline s; let pa = Pcoq.Gram.parsable (Stream.of_string s) in let pe = Pcoq.Gram.Entry.parse Pcoq.main_entry pa in - (* Temporary hack to make coqide.byte work (WTF???) *) - Pervasives.prerr_endline ""; - match pe with + (* Temporary hack to make coqide.byte work (WTF???) - now with less screen + * pollution *) + Pervasives.prerr_string " \r"; Pervasives.flush stderr; + match pe with | None -> assert false | Some((loc,vernac) as last) -> if is_vernac_debug_command vernac then @@ -435,58 +422,28 @@ let interp_with_options verbosely options s = 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 + 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 + let reset_info = compute_reset_info last 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 + reset_info let interp verbosely phrase = interp_with_options verbosely (make_option_commands ()) phrase -let interp_and_replace s = +let interp_and_replace s = let result = interp false s in let msg = read_stdout () in result,msg -let nb_subgoals pf = - List.length (fst (Refiner.frontier (Tacmach.proof_of_pftreestate pf))) - -type tried_tactic = - | Interrupted - | Success of int (* nb of goals after *) - | Failed - -let try_interptac s = - try - prerr_endline ("Starting try_interptac: "^s); - let pf = get_pftreestate () in - let pe = Pcoq.Gram.Entry.parse - Pcoq.main_entry - (Pcoq.Gram.parsable (Stream.of_string s)) - in match pe with - | Some (loc,(VernacSolve (n, tac, _))) -> - let tac = Tacinterp.interp tac in - let pf' = solve_nth_pftreestate n tac pf in - prerr_endline "Success"; - let nb_goals = nb_subgoals pf' - nb_subgoals pf in - Success nb_goals - | _ -> - prerr_endline "try_interptac: not a tactic"; Failed - with - | Sys.Break | Stdpp.Exc_located (_,Sys.Break) - -> prerr_endline "try_interp: interrupted"; Interrupted - | Stdpp.Exc_located (_,e) -> prerr_endline ("try_interp: failed ("^(Printexc.to_string e)); Failed - | e -> Failed - let rec is_pervasive_exn = function | Out_of_memory | Stack_overflow | Sys.Break -> true | Error_in_file (_,_,e) -> is_pervasive_exn e @@ -499,7 +456,7 @@ let print_toplevel_error exc = match exc with | DuringCommandInterp (loc,ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) - | _ -> (None, exc) + | _ -> (None, exc) in let (loc,exc) = match exc with @@ -509,19 +466,17 @@ let print_toplevel_error exc = in match exc with | End_of_input -> str "Please report: End of input",None - | Vernacexpr.ProtectedLoop -> - str "ProtectedLoop not allowed by coqide!",None | Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None | Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None - | _ -> - (try Cerrors.explain_exn exc with e -> + | _ -> + (try Cerrors.explain_exn exc with e -> str "Failed to explain error. This is an internal Coq error. Please report.\n" ++ str (Printexc.to_string e)), (if is_pervasive_exn exc then None else loc) let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc) -let interp_last last = +let interp_last last = prerr_string "*"; try vernac_com (States.with_heavy_rollback Vernacentries.interp) last; @@ -530,9 +485,89 @@ let interp_last last = let s,_ = process_exn e in prerr_endline ("Replay during undo failed because: "^s); raise e +let push_phrase cmd_stk reset_info ide_payload = + Stack.push (ide_payload,reset_info) cmd_stk + +type backtrack = + | BacktrackToNextActiveMark + | BacktrackToMark of reset_mark + | NoBacktrack + +let apply_reset = function + | BacktrackToMark mark -> reset_to mark + | NoBacktrack -> () + | BacktrackToNextActiveMark -> assert false + +let rewind sequence cmd_stk = + let undo_ops = Hashtbl.create 31 in + let current_proofs = undo_info () in + let pop_state cont seq coq reset_op prev_proofs curprf = + prerr_endline "pop"; + let curprf = + Option.map + (fun (curprf,depth) -> + (if Hashtbl.mem undo_ops curprf then Hashtbl.replace else Hashtbl.add) + undo_ops curprf depth; + curprf) + coq.cur_prf in + let reset_op = + match coq.status with + | ResetAtRegisteredObject mark -> + BacktrackToMark mark + | _ when is_vernac_state_preserving_command (snd coq.loc_ast) -> + reset_op + | _ when is_vernac_tactic_command (snd coq.loc_ast) -> + reset_op + | _ -> + BacktrackToNextActiveMark in + cont seq reset_op coq.proofs curprf + in + let rec do_rewind seq reset_op prev_proofs curprf = + match seq with + | [] when ((reset_op <> BacktrackToNextActiveMark) && + (Util.list_subset prev_proofs current_proofs)) -> + begin + Hashtbl.iter + (fun id depth -> + if List.mem id prev_proofs then begin + Pfedit.resume_proof (Util.dummy_loc,id); + Pfedit.undo_todepth depth + end) + undo_ops; + prerr_endline "OK for undos"; + Option.iter (fun id -> if List.mem id prev_proofs then + Pfedit.resume_proof (Util.dummy_loc,id)) curprf; + prerr_endline "OK for focusing"; + List.iter + (fun id -> Pfedit.delete_proof (Util.dummy_loc,id)) + (Util.list_subtract current_proofs prev_proofs); + prerr_endline "OK for aborts"; + apply_reset reset_op; + prerr_endline "OK for reset" + end + | [] -> + begin + try + let ide,coq = Stack.pop cmd_stk in + pop_state do_rewind [] coq reset_op prev_proofs curprf; + prerr_endline "push"; + let reset_info = compute_reset_info coq.loc_ast in + interp_last coq.loc_ast; + push_phrase cmd_stk reset_info ide + with Stack.Empty -> reset_initial () + end + | coq::rem -> + pop_state do_rewind rem coq reset_op prev_proofs curprf + in + do_rewind sequence NoBacktrack current_proofs None + +type tried_tactic = + | Interrupted + | Success of int (* nb of goals after *) + | Failed type hyp = env * evar_map * - ((identifier * string) * constr option * constr) * + ((identifier * string) * constr option * constr) * (string * string) type concl = env * evar_map * constr * string type meta = env * evar_map * string @@ -540,7 +575,7 @@ type goal = hyp list * concl let prepare_hyp sigma env ((i,c,d) as a) = env, sigma, - ((i,string_of_id i),c,d), + ((i,string_of_id i),c,d), (msg (pr_var_decl env a), msg (pr_ltype_env env d)) let prepare_hyps sigma env = @@ -548,7 +583,7 @@ let prepare_hyps sigma env = let hyps = fold_named_context (fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc) - env ~init:[] + env ~init:[] in List.rev hyps @@ -571,74 +606,66 @@ let get_current_pm_goal () = let gl = sig_it gls in prepare_goal sigma gl - -let get_current_goals () = +let get_current_goals () = let pfts = get_pftreestate () in - let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in + let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in let sigma = Tacmach.evc_of_pftreestate pfts in List.map (prepare_goal sigma) gls -let get_current_goals_nb () = - try List.length (get_current_goals ()) with _ -> 0 - let print_no_goal () = - let pfts = get_pftreestate () in - let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in - assert (gls = []); - let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in - msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls) - + (* Fall back on standard coq goal printer for completed goal printing *) + msg (pr_open_subgoals ()) let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = [("clear "^ident),("clear "^ident^"."); - + ("apply "^ident), ("apply "^ident^"."); - + ("exact "^ident), ("exact "^ident^"."); ("generalize "^ident), ("generalize "^ident^"."); - + ("absurd <"^ident^">"), ("absurd "^ pr_ast ^".") ] @ - (if is_equation ast then + (if is_equality_type ast then [ "discriminate "^ident, "discriminate "^ident^"."; "injection "^ident, "injection "^ident^"." ] else []) @ - + (let _,t = splay_prod env sigma ast in - if is_equation t then + if is_equality_type t then [ "rewrite "^ident, "rewrite "^ident^"."; "rewrite <- "^ident, "rewrite <- "^ident^"." ] else []) @ - + [("elim "^ident), ("elim "^ident^"."); - + ("inversion "^ident), ("inversion "^ident^"."); - + ("inversion clear "^ident), - ("inversion_clear "^ident^".")] + ("inversion_clear "^ident^".")] -let concl_menu (_,_,concl,_) = - let is_eq = is_equation concl in +let concl_menu (_,_,concl,_) = + let is_eq = is_equality_type concl in ["intro", "intro."; "intros", "intros."; "intuition","intuition." ] @ - - (if is_eq then + + (if is_eq then ["reflexivity", "reflexivity."; "discriminate", "discriminate."; "symmetry", "symmetry." ] - else + else []) @ ["assumption" ,"assumption."; @@ -660,43 +687,44 @@ let concl_menu (_,_,concl,_) = ] -let id_of_name = function - | Names.Anonymous -> id_of_string "x" +let id_of_name = function + | Names.Anonymous -> id_of_string "x" | Names.Name x -> x -let make_cases s = +let make_cases s = let qualified_name = Libnames.qualid_of_string s in let glob_ref = Nametab.locate qualified_name in match glob_ref with - | Libnames.IndRef i -> + | Libnames.IndRef i -> let {Declarations.mind_nparams = np}, {Declarations.mind_consnames = carr ; - Declarations.mind_nf_lc = tarr } - = Global.lookup_inductive i + Declarations.mind_nf_lc = tarr } + = Global.lookup_inductive i in - Util.array_fold_right2 - (fun n t l -> + Util.array_fold_right2 + (fun n t l -> let (al,_) = Term.decompose_prod t in let al,_ = Util.list_chop (List.length al - np) al in - let rec rename avoid = function + let rec rename avoid = function | [] -> [] - | (n,_)::l -> - let n' = next_global_ident_away true - (id_of_name n) + | (n,_)::l -> + let n' = next_ident_away_in_goal + (id_of_name n) avoid in (string_of_id n')::(rename (n'::avoid) l) in let al' = rename [] (List.rev al) in (string_of_id n :: al') :: l ) - carr + carr tarr [] | _ -> raise Not_found -let current_status () = +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 a1bea931..5cf66d36 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq.mli 11126 2008-06-13 18:45:04Z herbelin $ i*) +(*i $Id$ i*) open Names open Term @@ -29,31 +29,19 @@ type printing_state = { val printing_state : printing_state -type reset_mark = - | ResetToId of Names.identifier - | ResetToState of Libnames.object_name +type reset_info -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 -> reset_info * (Util.loc * Vernacexpr.vernac_expr) +val init : unit -> string list +val interp : bool -> string -> reset_info val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit -val interp_and_replace : string -> - (reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string +val interp_and_replace : string -> + reset_info * string + +val push_phrase : ('a * reset_info) Stack.t -> reset_info -> 'a -> unit + +val rewind : reset_info list -> ('a * reset_info) Stack.t -> unit val is_vernac_tactic_command : Vernacexpr.vernac_expr -> bool val is_vernac_state_preserving_command : Vernacexpr.vernac_expr -> bool @@ -62,7 +50,7 @@ val is_vernac_proof_ending_command : Vernacexpr.vernac_expr -> bool (* type hyp = (identifier * constr option * constr) * string *) -type hyp = env * evar_map * +type hyp = env * evar_map * ((identifier*string) * constr option * constr) * (string * string) type meta = env * evar_map * string type concl = env * evar_map * constr * string @@ -72,8 +60,6 @@ val get_current_goals : unit -> goal list val get_current_pm_goal : unit -> goal -val get_current_goals_nb : unit -> int - val print_no_goal : unit -> string val process_exn : exn -> string*(Util.loc option) @@ -88,13 +74,11 @@ val is_in_loadpath : string -> bool val make_cases : string -> string list list -type tried_tactic = +type tried_tactic = | Interrupted | Success of int (* nb of goals after *) | Failed -val try_interptac: string -> tried_tactic - (* Message to display in lower status bar. *) val current_status : unit -> string diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 3a48fc7d..e4a3ae56 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 10994 2008-05-26 16:21:31Z jnarboux $ *) +(* $Id$ *) let commands = [ [(* "Abort"; *) @@ -43,7 +43,7 @@ let commands = [ ]; ["End"; "End Silent."; - "Eval"; + "Eval"; "Extract Constant"; "Extract Inductive"; "Extraction Inline"; @@ -84,7 +84,7 @@ let commands = [ ["Parameter"; "Proof."; "Program Definition"; - "Program Fixpoint"; + "Program Fixpoint"; "Program Lemma"; "Program Theorem"; ]; @@ -100,7 +100,7 @@ let commands = [ "Require Export"; "Require Import"; "Reset Extraction Inline"; - "Restore State"; + "Restore State"; ]; [ "Save."; "Scheme"; @@ -155,6 +155,7 @@ let commands = [ ] let state_preserving = [ + "About"; "Check"; "Eval"; "Eval lazy in"; @@ -165,7 +166,7 @@ let state_preserving = [ "Extraction Module"; "Inspect"; "Locate"; - + "Obligations"; "Print"; "Print All."; @@ -191,7 +192,7 @@ let state_preserving = [ "Print Scope"; "Print Scopes."; "Print Section"; - + "Print Table Printing If."; "Print Table Printing Let."; "Print Tables."; @@ -229,7 +230,7 @@ let state_preserving = [ ] -let tactics = +let tactics = [ [ "abstract"; @@ -316,7 +317,7 @@ let tactics = "generalize"; "generalize dependent"; ]; - + [ "hnf"; ]; @@ -415,7 +416,7 @@ let tactics = "trivial"; "try"; ]; - + [ "unfold"; "unfold __ in"; diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll new file mode 100644 index 00000000..03ce950f --- /dev/null +++ b/ide/coq_lex.mll @@ -0,0 +1,194 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Hashtbl.add h s ()) + [ "Add" ; "Check"; "Eval"; "Extraction" ; + "Load" ; "Undo"; "Goal"; + "Proof" ; "Print";"Save" ; + "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" + ]; + Hashtbl.mem h + + let is_constr_kw = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; + "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return"; + "Prop"; "Set"; "Type" ]; + Hashtbl.mem h + + (* 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 ()) + [ (* Definitions *) + "Definition" ; "Let" ; "Example" ; "SubClass" ; + "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ; + (* Assumptions *) + "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; + "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"; + (* Inductive *) + "Inductive" ; "CoInductive" ; "Record" ; "Structure" ; + (* Other *) + "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" + ]; + Hashtbl.mem h + + let is_proof_declaration = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ; + "Proposition" ; "Property" ]; + Hashtbl.mem h + + let is_proof_end = + let h = Hashtbl.create 97 in + List.iter (fun s -> Hashtbl.add h s ()) + [ "Qed" ; "Defined" ; "Admitted" ]; + Hashtbl.mem h + + let start = ref true +} + +let space = + [' ' '\010' '\013' '\009' '\012'] + +let firstchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'] +let identchar = + ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] +let ident = firstchar identchar* + +let sentence_sep = '.' [ ' ' '\n' '\t' ] + +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" +| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))| + ("Library"|"Inline"|"NoInline"|"Blacklist")) +| "Recursive" space+ "Extraction" (space+ "Library")? +| ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist") +| "Extract" space+ (("Inlined" space+) "Constant"| "Inductive") + +(* At least still missing: "Inline" + decl, variants of "Identity + Coercion", variants of Print, Add, ... *) + +rule coq_string = parse + | "\"\"" { coq_string lexbuf } + | "\"" { Lexing.lexeme_end lexbuf } + | eof { Lexing.lexeme_end lexbuf } + | _ { coq_string lexbuf } + +and comment = parse + | "(*" { ignore (comment lexbuf); comment lexbuf } + | "\"" { ignore (coq_string lexbuf); comment lexbuf } + | "*)" { Lexing.lexeme_end lexbuf } + | eof { Lexing.lexeme_end lexbuf } + | _ { comment lexbuf } + +and sentence stamp = parse + | space+ { sentence stamp lexbuf } + | "(*" { + let comm_start = Lexing.lexeme_start lexbuf in + let comm_end = comment lexbuf in + stamp comm_start comm_end Comment; + sentence stamp lexbuf + } + | "\"" { + let str_start = Lexing.lexeme_start lexbuf in + let str_end = coq_string lexbuf in + stamp str_start str_end String; + start := false; + sentence stamp lexbuf + } + | multiword_declaration { + if !start then begin + start := false; + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration + end; + sentence stamp lexbuf + } + | multiword_command { + if !start then begin + start := false; + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword + end; + sentence stamp lexbuf } + | ident as id { + if !start then begin + start := false; + if id <> "Time" then begin + if is_proof_end id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Qed + else if is_one_word_command id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword + else if is_one_word_declaration id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration + else if is_proof_declaration id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) ProofDeclaration + end + end else begin + if is_constr_kw id then + stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword + end; + sentence stamp lexbuf } + | ".." + | _ { sentence stamp lexbuf} + | sentence_sep { } + | eof { raise Not_found } + +{ + let find_end_offset stamp slice = + let lb = Lexing.from_string slice in + start := true; + sentence stamp lb; + Lexing.lexeme_end lb +} diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml index 92d2de78..c6e1f1a4 100644 --- a/ide/coq_tactics.ml +++ b/ide/coq_tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_tactics.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id$ *) let tactics = [ "Abstract"; diff --git a/ide/coq_tactics.mli b/ide/coq_tactics.mli index 05e233eb..c31933ba 100644 --- a/ide/coq_tactics.mli +++ b/ide/coq_tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coq_tactics.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id$ i*) val tactics : string list diff --git a/ide/coqide.ml b/ide/coqide.ml index cc147d5e..201fbe47 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -7,123 +7,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *) +(* $Id$ *) open Preferences open Vernacexpr open Coq +open Gtk_parsing open Ideutils - -let cb_ = ref None -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 () = Option.get !_notebook +type ide_info = { + start : GText.mark; + stop : GText.mark; +} -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 *) -let decompose_tab w = - let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in - let l = vbox#children in - match l with - | [img;lbl] -> - let img = new GMisc.image - ((Gobject.try_cast img#as_widget "GtkImage"): - Gtk.image Gtk.obj) - in - let lbl = GMisc.label_cast lbl in - vbox,img,lbl - | _ -> assert false - -let set_tab_label i n = - let nb = notebook () in - let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - lbl#set_use_markup true; - (* lbl#set_text n *) lbl#set_label n - - -let set_tab_image ~icon i = - let nb = notebook () in - let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - img#set_icon_size `SMALL_TOOLBAR; - img#set_stock icon - -let set_current_tab_image ~icon = set_tab_image ~icon (notebook())#current_page - -let set_current_tab_label n = set_tab_label (notebook())#current_page n - -let get_tab_label i = - let nb = notebook () in - let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - lbl#text - -let get_full_tab_label i = - let nb = notebook () in - let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - lbl - -let get_current_tab_label () = get_tab_label (notebook())#current_page - -let get_current_page () = - let i = (notebook())#current_page in - (notebook())#get_nth_page i - -(* This function must remove "focused proof" decoration *) -let reset_tab_label i = - set_tab_label i (get_tab_label i) - -let to_do_on_page_switch = ref [] - -module Vector = struct - exception Found of int - type 'a t = ('a option) array ref - let create () = ref [||] - let length t = Array.length !t - 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 - let iter f t = Array.iter (function | None -> () | Some x -> f x) !t - let find_or_fail f t = - let test i = function | None -> () | Some e -> if f e then raise (Found i) in - Array.iteri test t - - let exists f t = - let l = Array.length !t in - let rec test i = - (i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1)) - in - test 0 -end -type 'a viewable_script = - {view : Undo.undoable_view; - mutable analyzed_view : 'a option; - } - - -class type analyzed_views= +class type analyzed_views= object('self) val mutable act_id : GtkSignal.id option - val current_all : 'self viewable_script val mutable deact_id : GtkSignal.id option val input_buffer : GText.buffer val input_view : Undo.undoable_view @@ -133,6 +33,7 @@ object('self) val message_view : GText.view val proof_buffer : GText.buffer val proof_view : GText.view + val cmd_stack : (ide_info * Coq.reset_info) Stack.t val mutable is_active : bool val mutable read_only : bool val mutable filename : string option @@ -145,7 +46,6 @@ object('self) method add_detached_view : GWindow.window -> unit method remove_detached_view : GWindow.window -> unit - method view : Undo.undoable_view method filename : string option method stats : Unix.stats option method set_filename : string option -> unit @@ -184,7 +84,7 @@ object('self) method send_to_coq : bool -> bool -> string -> bool -> bool -> bool -> - (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option + (bool*reset_info) option method set_message : string -> unit method show_pm_goal : unit method show_goals : unit @@ -192,37 +92,132 @@ object('self) method undo_last_step : unit method help_for_keyword : unit -> unit method complete_at_offset : int -> bool - - method blaster : unit -> unit end -let (input_views:analyzed_views viewable_script Vector.t) = Vector.create () + +type viewable_script = + {script : Undo.undoable_view; + tab_label : GMisc.label; + mutable filename : string; + mutable encoding : string; + proof_view : GText.view; + message_view : GText.view; + analyzed_view : analyzed_views; + command_stack : (ide_info * Coq.reset_info) Stack.t; + } + + +let notebook_page_of_session {script=script;tab_label=bname;proof_view=proof;message_view=message} = + let session_paned = + GPack.paned `HORIZONTAL ~border_width:5 () in + let script_frame = + GBin.frame ~shadow_type:`IN ~packing:session_paned#add1 () in + let script_scroll = + GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in + let state_paned = + GPack.paned `VERTICAL ~packing:session_paned#add2 () in + let proof_frame = + GBin.frame ~shadow_type:`IN ~packing:state_paned#add1 () in + let proof_scroll = + GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in + let message_frame = + GBin.frame ~shadow_type:`IN ~packing:state_paned#add2 () in + let message_scroll = + GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in + let session_tab = + GPack.hbox ~homogeneous:false () in + let img = + GMisc.image ~packing:session_tab#pack ~icon_size:`SMALL_TOOLBAR () in + let _ = + script#buffer#connect#modified_changed + ~callback:(fun () -> if script#buffer#modified + then img#set_stock `SAVE + else img#set_stock `YES) in + let _ = + session_paned#misc#connect#size_allocate + (let old_paned_width = ref 2 in + let old_paned_height = ref 2 in + (fun {Gtk.width=paned_width;Gtk.height=paned_height} -> + if !old_paned_width <> paned_width || !old_paned_height <> paned_height then ( + session_paned#set_position (session_paned#position * paned_width / !old_paned_width); + state_paned#set_position (state_paned#position * paned_height / !old_paned_height); + old_paned_width := paned_width; + old_paned_height := paned_height; + ))) in + script_scroll#add script#coerce; + proof_scroll#add proof#coerce; + message_scroll#add message#coerce; + session_tab#pack bname#coerce; + img#set_stock `YES; + session_paned#set_position 1; + state_paned#set_position 1; + (Some session_tab#coerce,None,session_paned#coerce) + +let session_notebook = + Typed_notebook.create notebook_page_of_session ~border_width:2 ~show_border:false ~scrollable:true () + +let active_view = ref (~-1) + +let on_active_view f = + if !active_view < 0 + then failwith "no active view !" + else f (session_notebook#get_nth_term !active_view) + +let cb = GData.clipboard Gdk.Atom.primary + + +let last_cb_content = ref "" -let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; - Sys.sigill; Sys.sigpipe; Sys.sigquit; +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 + session_notebook#set_tab_pos pos + + +let set_active_view i = + prerr_endline "entering set_active_view"; + (try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ()); + session_notebook#goto_page i; + let s = session_notebook#current_term in + s.tab_label#set_use_markup true; + s.tab_label#set_label (""^s.tab_label#text^""); + active_view := i; + prerr_endline "exiting set_active_view" + + + +let to_do_on_page_switch = ref [] + + +let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; + Sys.sigill; Sys.sigpipe; Sys.sigquit; (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2] let crash_save i = (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*) Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files"; - let count = ref 0 in - Vector.iter - (function {view=view; analyzed_view = Some av } -> - (let filename = match av#filename with - | None -> - incr count; + let count = ref 0 in + List.iter + (function {script=view; analyzed_view = av } -> + (let filename = match av#filename with + | None -> + incr count; "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide" | Some f -> f^".crashcoqide" in - try + try if try_export filename (view#buffer#get_text ()) then Pervasives.prerr_endline ("Saved "^filename) else Pervasives.prerr_endline ("Could not save "^filename) with _ -> Pervasives.prerr_endline ("Could not save "^filename)) - | _ -> Pervasives.prerr_endline "Unanalyzed view found. Please report." ) - input_views; + session_notebook#pages; Pervasives.prerr_endline "Done. Please report."; if i <> 127 then exit i @@ -240,9 +235,9 @@ let coq_computing = Mutex.create () (* To prevent Coq from interrupting during undoing...*) let coq_may_stop = Mutex.create () -let break () = +let break () = prerr_endline "User break received:"; - if not (Mutex.try_lock coq_computing) then + if not (Mutex.try_lock coq_computing) then begin prerr_endline " trying to stop computation:"; if Mutex.try_lock coq_may_stop then begin @@ -256,225 +251,110 @@ let break () = prerr_endline " ignored (not computing)" end -let do_if_not_computing text f x = - let threaded_task () = - if Mutex.try_lock coq_computing - then - begin - let w = Blaster_window.blaster_window () in - if not (Mutex.try_lock w#lock) then - begin - break (); - let lck = Mutex.create () in - Mutex.lock lck; - prerr_endline "Waiting on blaster..."; - Condition.wait w#blaster_killed lck; - prerr_endline "Waiting on blaster ok"; - Mutex.unlock lck - end - else - Mutex.unlock w#lock; - let idle = - Glib.Timeout.add ~ms:300 - ~callback:(fun () -> async !pulse ();true) in - begin - prerr_endline "Getting lock"; - try - f x; - Glib.Timeout.remove idle; - prerr_endline "Releasing lock"; - Mutex.unlock coq_computing; - with e -> - Glib.Timeout.remove idle; - prerr_endline "Releasing lock (on error)"; - Mutex.unlock coq_computing; - raise e - end - end - else - prerr_endline - "Discarded order (computations are ongoing)" - in - prerr_endline ("Launching thread " ^ text); - ignore (Thread.create threaded_task ()) - -let add_input_view tv = - Vector.append input_views tv - -let get_input_view i = - if 0 <= i && i < Vector.length input_views - then - Vector.get input_views i - else raise Not_found - -let active_view = ref None - -let get_active_view () = Vector.get input_views (Option.get !active_view) - -let set_active_view i = - (match !active_view with None -> () | Some i -> - reset_tab_label i); - (notebook ())#goto_page i; - let txt = get_current_tab_label () in - set_current_tab_label (""^txt^""); - active_view := Some i - -let set_current_view i = (notebook ())#goto_page i - -let kill_input_view i = - let v = Vector.get input_views i in - (match v.analyzed_view with - | Some v -> v#kill_detached_views () - | None -> ()); - v.view#destroy (); - v.analyzed_view <- None; - Vector.remove input_views i - -let get_current_view_page () = (notebook ())#current_page -let get_current_view () = Vector.get input_views (notebook ())#current_page -let remove_current_view_page () = - let c = (notebook ())#current_page in - kill_input_view c; - ((notebook ())#get_nth_page c)#misc#hide () - -let is_word_char c = - (* TODO: avoid num and prime at the head of a word *) - Glib.Unichar.isalnum c || c = underscore || c = prime - -let starts_word it = - prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'"); - (not it#copy#nocopy#backward_char || - (let c = it#backward_char#char in - not (is_word_char c))) - -let ends_word it = - (not it#copy#nocopy#forward_char || - let c = it#forward_char#char in - not (is_word_char c) - ) - -let inside_word it = - let c = it#char in - not (starts_word it) && - not (ends_word it) && - is_word_char c - -let is_on_word_limit it = inside_word it || ends_word it - -let rec find_word_start it = - prerr_endline "Find word start"; - if not it#nocopy#backward_char then - (prerr_endline "find_word_start: cannot backward"; it) - else if is_word_char it#char - then find_word_start it - else (it#nocopy#forward_char; - prerr_endline ("Word start at: "^(string_of_int it#offset));it) -let find_word_start (it:GText.iter) = find_word_start it#copy - -let rec find_word_end it = - prerr_endline "Find word end"; - if let c = it#char in c<>0 && is_word_char c - then begin - ignore (it#nocopy#forward_char); - find_word_end it - end else (prerr_endline ("Word end at: "^(string_of_int it#offset));it) -let find_word_end it = find_word_end it#copy - - -let get_word_around it = - let start = find_word_start it in - let stop = find_word_end it in - start,stop - - -let rec complete_backward w (it:GText.iter) = - prerr_endline "Complete backward..."; - match it#backward_search w with - | None -> (prerr_endline "backward_search failed";None) - | Some (start,stop) -> - prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset)); - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 - then complete_backward w start - else Some (start,stop,ne) - else complete_backward w start - -let rec complete_forward w (it:GText.iter) = - prerr_endline "Complete forward..."; - match it#forward_search w with - | None -> None - | Some (start,stop) -> - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 then - complete_forward w stop - else Some (stop,stop,ne) - else complete_forward w stop +let do_if_not_computing text f x = + if Mutex.try_lock coq_computing then + let threaded_task () = + prerr_endline "Getting lock"; + try + f x; + prerr_endline "Releasing lock"; + Mutex.unlock coq_computing; + with e -> + prerr_endline "Releasing lock (on error)"; + Mutex.unlock coq_computing; + raise e + in + prerr_endline ("Launching thread " ^ text); + ignore (Glib.Timeout.add ~ms:300 ~callback: + (fun () -> if Mutex.try_lock coq_computing + then (Mutex.unlock coq_computing; false) + else (pbar#pulse (); true))); + ignore (Thread.create threaded_task ()) + else + prerr_endline + "Discarded order (computations are ongoing)" + +(* XXX - 1 appel *) +let kill_input_view i = + let v = session_notebook#get_nth_term i in + v.analyzed_view#kill_detached_views (); + v.script#destroy (); + v.tab_label#destroy (); + v.proof_view#destroy (); + v.message_view#destroy (); + session_notebook#remove_page i +(* +(* XXX - beaucoups d'appels, a garder *) +let get_current_view = + focused_session + *) +let remove_current_view_page () = + let c = session_notebook#current_page in + kill_input_view c + (* Reset this to None on page change ! *) let (last_completion:(string*int*int*bool) option ref) = ref None -let () = to_do_on_page_switch := +let () = to_do_on_page_switch := (fun i -> last_completion := None)::!to_do_on_page_switch let rec complete input_buffer w (offset:int) = - match !last_completion with + match !last_completion with | Some (lw,loffset,lpos,backward) when lw=w && loffset=offset -> begin let iter = input_buffer#get_iter (`OFFSET lpos) in - if backward then + if backward then match complete_backward w iter with - | None -> - last_completion := + | None -> + last_completion := Some (lw,loffset, - (find_word_end + (find_word_end (input_buffer#get_iter (`OFFSET loffset)))#offset , - false); + false); None - | Some (ss,start,stop) as result -> - last_completion := + | Some (ss,start,stop) as result -> + last_completion := Some (w,offset,ss#offset,true); result else match complete_forward w iter with - | None -> + | None -> last_completion := None; None - | Some (ss,start,stop) as result -> - last_completion := + | Some (ss,start,stop) as result -> + last_completion := Some (w,offset,ss#offset,false); result end | _ -> begin match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with - | None -> - last_completion := + | None -> + last_completion := Some (w,offset,(find_word_end (input_buffer#get_iter (`OFFSET offset)))#offset,false); complete input_buffer w offset - | Some (ss,start,stop) as result -> + | Some (ss,start,stop) as result -> last_completion := Some (w,offset,ss#offset,true); result end - + let get_current_word () = - let av = Option.get ((get_current_view ()).analyzed_view) in - match (cb ())#text with - | None -> + match session_notebook#current_term,cb#text with + | {script=script; analyzed_view=av;},None -> prerr_endline "None selected"; let it = av#get_insert in let start = find_word_start it in let stop = find_word_end start in - av#view#buffer#move_mark `SEL_BOUND start; - av#view#buffer#move_mark `INSERT stop; - av#view#buffer#get_text ~slice:true ~start ~stop () - | Some t -> + script#buffer#move_mark `SEL_BOUND start; + script#buffer#move_mark `INSERT stop; + script#buffer#get_text ~slice:true ~start ~stop () + | _,Some t -> prerr_endline "Some selected"; prerr_endline t; t - + let input_channel b ic = let buf = String.create 1024 and len = ref 0 in @@ -488,142 +368,6 @@ let with_file handler name ~f = 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; - ast:Util.loc * Vernacexpr.vernac_expr; - reset_info:Coq.reset_info - } - -exception Size of int -let (processed_stack:info Stack.t) = Stack.create () -let push x = Stack.push x processed_stack -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_segment id = - let lookup_section = function - | { 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 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 = reset_info - } in - begin - match snd ast with - | VernacEndSegment (_,id) -> - prerr_endline "Updating on end of segment 1"; - update_on_end_of_segment id - | _ -> () - end; - push x - - -let repush_phrase reset_info x = - let x = { x with reset_info = reset_info } in - begin - match snd x.ast with - | 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 as x) = - if q = 0 then x else (n,a,BacktrackToNextActiveMark,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 apply_aborts a = - 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 - -exception UndoStackExhausted - -let apply_tactic_undo n = - if n<>0 then - (prerr_endline ("Applying "^string_of_int n^" undos"); - try Pfedit.undo n with _ -> raise UndoStackExhausted) - -let apply_reset = function - | BacktrackToMark mark -> reset_to mark - | BacktrackToModSec id -> reset_to_mod id - | NoBacktrack -> () - | BacktrackToNextActiveMark -> assert false - -let rec apply_undos (n,a,b,p,l as undos) = - if p = 0 & b <> BacktrackToNextActiveMark then - begin - apply_aborts a; - try - apply_tactic_undo n; - apply_reset b - with UndoStackExhausted -> - apply_undos (n,0,BacktrackToNextActiveMark,p,l) - end - else - (* re-synchronize Coq to the current state of the stack *) - if is_empty () then - Coq.reset_initial () - else - begin - let t = top () in - apply_undos (pop_command undos t); - let reset_info = Coq.compute_reset_info (snd t.ast) in - interp_last t.ast; - repush_phrase reset_info t - end (* For electric handlers *) exception Found @@ -631,19 +375,16 @@ exception Found (* For find_phrase_starting_at *) exception Stop of int -let activate_input i = - (match !active_view with - | None -> () - | Some n -> - let a_v = Option.get (Vector.get input_views n).analyzed_view in - a_v#deactivate (); - a_v#reset_initial - ); - let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in - activate_function (); - set_active_view i - -let warning msg = +(* XXX *) +let activate_input i = + prerr_endline "entering activate_input"; + (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ()) + with _ -> ()); + (session_notebook#get_nth_term i).analyzed_view#activate (); + set_active_view i; + prerr_endline "exiting activate_input" + +let warning msg = GToolbox.message_box ~title:"Warning" ~icon:(let img = GMisc.image () in img#set_stock `DIALOG_WARNING; @@ -651,30 +392,142 @@ let warning msg = img#coerce) msg - -class analyzed_view index = - let {view = input_view_} as current_all_ = get_input_view index in - let proof_view_ = Option.get !proof_view in - let message_view_ = Option.get !message_view in +let apply_tag (buffer:GText.buffer) orig off_conv from upto sort = + let conv_and_apply start stop tag = + let start = orig#forward_chars (off_conv from) in + let stop = orig#forward_chars (off_conv upto) in + buffer#apply_tag ~start ~stop tag + in match sort with + | Coq_lex.Comment -> + conv_and_apply from upto Tags.Script.comment + | Coq_lex.Keyword -> + conv_and_apply from upto Tags.Script.kwd + | Coq_lex.Declaration -> + conv_and_apply from upto Tags.Script.decl + | Coq_lex.ProofDeclaration -> + conv_and_apply from upto Tags.Script.proof_decl + | Coq_lex.Qed -> + conv_and_apply from upto Tags.Script.qed + | Coq_lex.String -> () + +let remove_tags (buffer:GText.buffer) from upto = + List.iter (buffer#remove_tag ~start:from ~stop:upto) + [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl; + Tags.Script.proof_decl; Tags.Script.qed ] + +let split_slice_lax (buffer:GText.buffer) from upto = + remove_tags buffer from upto; + buffer#remove_tag ~start:from ~stop:upto Tags.Script.lax_end; + let slice = buffer#get_text ~start:from ~stop:upto () in + let slice = slice ^ " " in + let rec split_substring str = + let off_conv = byte_offset_to_char_offset str in + let slice_len = String.length str in + let sentence_len = Coq_lex.find_end_offset (apply_tag buffer from off_conv) str in + + let stop = from#forward_chars (pred (off_conv sentence_len)) in + let start = stop#backward_char in + buffer#apply_tag ~start ~stop Tags.Script.lax_end; + + if 1 < slice_len - sentence_len then begin (* remember that we added a trailing space *) + ignore (from#nocopy#forward_chars (off_conv sentence_len)); + split_substring (String.sub str sentence_len (slice_len - sentence_len)) + end + in + split_substring slice + +let rec grab_safe_sentence_start (iter:GText.iter) soi = + let lax_back = iter#backward_char#has_tag Tags.Script.lax_end in + let on_space = List.mem iter#char [0x09;0x0A;0x20] in + let full_ending = iter#is_start || (lax_back & on_space) in + if full_ending then iter + else if iter#compare soi <= 0 then raise Not_found + else + let prev = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in + (if prev#has_tag Tags.Script.lax_end then + ignore (prev#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end))); + grab_safe_sentence_start prev soi + +let grab_sentence_end_from (start:GText.iter) = + let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in + stop#forward_char + +let get_sentence_bounds (iter:GText.iter) = + let start = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in + (if start#has_tag Tags.Script.lax_end then ignore ( + start#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end))); + let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in + let stop = stop#forward_char in + start,stop + +let end_tag_present end_iter = + end_iter#backward_char#has_tag Tags.Script.lax_end + +let tag_on_insert = + let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *) + fun buffer -> + try + let insert = buffer#get_iter_at_mark `INSERT in + let start = grab_safe_sentence_start insert + (buffer#get_iter_at_mark (`NAME "start_of_input")) in + let stop = grab_sentence_end_from insert in + let skip_curr = ref true in (* shall the callback be skipped ? by default yes*) + (!skip_last) := true; (* skip the previously created callback *) + skip_last := skip_curr; + try split_slice_lax buffer start stop + with Not_found -> + skip_curr := false; + ignore (Glib.Timeout.add ~ms:1500 + ~callback:(fun () -> if not !skip_curr then ( + try split_slice_lax buffer start buffer#end_iter with _ -> ()); false)) + with Not_found -> + let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in + buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char + +let force_retag buffer = + try split_slice_lax buffer buffer#start_iter buffer#end_iter with _ -> () + +let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = + (* move back twice if not into proof_decl, + * once if into proof_decl and back_char into_proof_decl, + * don't move if into proof_decl and back_char not into proof_decl *) + if not (cursor#has_tag Tags.Script.proof_decl) then + ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); + if cursor#backward_char#has_tag Tags.Script.proof_decl then + ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); + let decl_start = cursor in + let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in + let decl_end = grab_sentence_end_from decl_start in + let prf_end = grab_sentence_end_from prf_end in + let prf_end = prf_end#forward_char in + if decl_start#has_tag Tags.Script.folded then ( + buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; + buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) + else ( + buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; + buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) + +class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs = object(self) - val current_all = current_all_ - val input_view = current_all_.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 + val input_view = _script + val input_buffer = _script#buffer + val proof_view = _pv + val proof_buffer = _pv#buffer + val message_view = _mv + val message_buffer = _mv#buffer + val cmd_stack = _cs val mutable is_active = false val mutable read_only = false - val mutable filename = None + val mutable filename = None val mutable stats = None val mutable last_modification_time = 0. val mutable last_auto_save_time = 0. val mutable detached_views = [] val mutable auto_complete_on = !current.auto_complete + val hidden_proofs = Hashtbl.create 32 - method private toggle_auto_complete = + method private toggle_auto_complete = auto_complete_on <- not auto_complete_on method set_auto_complete t = auto_complete_on <- t method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x -> @@ -683,131 +536,130 @@ object(self) let y = f x in self#set_auto_complete old; y - method add_detached_view (w:GWindow.window) = + method add_detached_view (w:GWindow.window) = detached_views <- w::detached_views - method remove_detached_view (w:GWindow.window) = + method remove_detached_view (w:GWindow.window) = detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views - method kill_detached_views () = + method kill_detached_views () = List.iter (fun w -> w#destroy ()) detached_views; detached_views <- [] - method view = input_view method filename = filename method stats = stats - method set_filename f = + method set_filename f = filename <- f; - match f with + match f with | Some f -> stats <- my_stat f | None -> () - method update_stats = - match filename with - | Some f -> stats <- my_stat f + method update_stats = + match filename with + | Some f -> stats <- my_stat f | _ -> () - method revert = - match filename with + method revert = + match filename with | Some f -> begin - let do_revert () = begin - !push_info "Reverting buffer"; - try - if is_active then self#reset_initial; - let b = Buffer.create 1024 in - 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; - input_buffer#place_cursor input_buffer#start_iter; - input_buffer#set_modified false; - !pop_info (); - !flash_info "Buffer reverted"; - Highlight.highlight_all input_buffer; - with _ -> - !pop_info (); - !flash_info "Warning: could not revert buffer"; - end - in - if input_buffer#modified then - match (GToolbox.question_box - ~title:"Modified buffer changed on disk" - ~buttons:["Revert from File"; - "Overwrite File"; - "Disable Auto Revert"] - ~default:0 - ~icon:(stock_to_widget `DIALOG_WARNING) - "Some unsaved buffers changed on disk" - ) - with 1 -> do_revert () - | 2 -> if self#save f then !flash_info "Overwritten" else - !flash_info "Could not overwrite file" - | _ -> - prerr_endline "Auto revert set to false"; - !current.global_auto_revert <- false; - disconnect_revert_timer () - else do_revert () - end + let do_revert () = begin + push_info "Reverting buffer"; + try + if is_active then self#reset_initial; + let b = Buffer.create 1024 in + 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; + input_buffer#place_cursor input_buffer#start_iter; + input_buffer#set_modified false; + pop_info (); + flash_info "Buffer reverted"; + force_retag input_buffer; + with _ -> + pop_info (); + flash_info "Warning: could not revert buffer"; + end + in + if input_buffer#modified then + match (GToolbox.question_box + ~title:"Modified buffer changed on disk" + ~buttons:["Revert from File"; + "Overwrite File"; + "Disable Auto Revert"] + ~default:0 + ~icon:(stock_to_widget `DIALOG_WARNING) + "Some unsaved buffers changed on disk" + ) + with 1 -> do_revert () + | 2 -> if self#save f then flash_info "Overwritten" else + flash_info "Could not overwrite file" + | _ -> + prerr_endline "Auto revert set to false"; + !current.global_auto_revert <- false; + disconnect_revert_timer () + else do_revert () + end | None -> () - - method save f = + + method save f = if try_export f (input_buffer#get_text ()) then begin - filename <- Some f; - input_buffer#set_modified false; - stats <- my_stat f; - (match self#auto_save_name with - | None -> () - | Some fn -> try Sys.remove fn with _ -> ()); - true - end + filename <- Some f; + input_buffer#set_modified false; + stats <- my_stat f; + (match self#auto_save_name with + | None -> () + | Some fn -> try Sys.remove fn with _ -> ()); + true + end else false - method private auto_save_name = - match filename with + method private auto_save_name = + match filename with | None -> None - | Some f -> - let dir = Filename.dirname f in - let base = (fst !current.auto_save_name) ^ - (Filename.basename f) ^ - (snd !current.auto_save_name) - in Some (Filename.concat dir base) - - method private need_auto_save = + | Some f -> + let dir = Filename.dirname f in + let base = (fst !current.auto_save_name) ^ + (Filename.basename f) ^ + (snd !current.auto_save_name) + in Some (Filename.concat dir base) + + method private need_auto_save = input_buffer#modified && - last_modification_time > last_auto_save_time - + last_modification_time > last_auto_save_time + method auto_save = if self#need_auto_save then begin - match self#auto_save_name with - | None -> () - | Some fn -> - try - last_auto_save_time <- Unix.time(); - prerr_endline ("Autosave time : "^(string_of_float (Unix.time()))); - if try_export fn (input_buffer#get_text ()) then begin - !flash_info ~delay:1000 "Autosaved" - end - else warning - ("Autosave failed (check if " ^ fn ^ " is writable)") - with _ -> - warning ("Autosave: unexpected error while writing "^fn) - end - + match self#auto_save_name with + | None -> () + | Some fn -> + try + last_auto_save_time <- Unix.time(); + prerr_endline ("Autosave time : "^(string_of_float (Unix.time()))); + if try_export fn (input_buffer#get_text ()) then begin + flash_info ~delay:1000 "Autosaved" + end + else warning + ("Autosave failed (check if " ^ fn ^ " is writable)") + with _ -> + warning ("Autosave: unexpected error while writing "^fn) + end + method save_as f = - if Sys.file_exists f then + if Sys.file_exists f then match (GToolbox.question_box ~title:"File exists on disk" - ~buttons:["Overwrite"; - "Cancel";] - ~default:1 - ~icon: - (let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - ("File "^f^"already exists") - ) + ~buttons:["Overwrite"; + "Cancel";] + ~default:1 + ~icon: + (let img = GMisc.image () in + img#set_stock `DIALOG_WARNING; + img#set_icon_size `DIALOG; + img#coerce) + ("File "^f^"already exists") + ) with 1 -> self#save f - | _ -> false - else self#save f + | _ -> false + else self#save f method set_read_only b = read_only<-b method read_only = read_only @@ -823,585 +675,494 @@ object(self) method clear_message = message_buffer#set_text "" val mutable last_index = true val last_array = [|"";""|] - method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input") + method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input") method get_insert = get_insert input_buffer - method recenter_insert = - (* BUG : to investigate further: - FIXED : Never call GMain.* in thread ! - PLUS : GTK BUG ??? Cannot be called from a thread... - ADDITION: using sync instead of async causes deadlock...*) + method recenter_insert = + (* BUG : to investigate further: + FIXED : Never call GMain.* in thread ! + PLUS : GTK BUG ??? Cannot be called from a thread... + ADDITION: using sync instead of async causes deadlock...*) ignore (GtkThread.async ( - input_view#scroll_to_mark - ~use_align:false - ~yalign:0.75 - ~within_margin:0.25) - `INSERT) + input_view#scroll_to_mark + ~use_align:false + ~yalign:0.75 + ~within_margin:0.25) + `INSERT) - method indent_current_line = + method indent_current_line = let get_nb_space it = let it = it#copy in let nb_sep = ref 0 in let continue = ref true in - while !continue do - if it#char = space then begin - incr nb_sep; - if not it#nocopy#forward_char then continue := false; - end else continue := false - done; - !nb_sep + while !continue do + if it#char = space then begin + incr nb_sep; + if not it#nocopy#forward_char then continue := false; + end else continue := false + done; + !nb_sep in let previous_line = self#get_insert in if previous_line#nocopy#backward_line then begin - let previous_line_spaces = get_nb_space previous_line in - let current_line_start = self#get_insert#set_line_offset 0 in - let current_line_spaces = get_nb_space current_line_start in - if input_buffer#delete_interactive - ~start:current_line_start - ~stop:(current_line_start#forward_chars current_line_spaces) - () - then - let current_line_start = self#get_insert#set_line_offset 0 in - input_buffer#insert - ~iter:current_line_start - (String.make previous_line_spaces ' ') - end + let previous_line_spaces = get_nb_space previous_line in + let current_line_start = self#get_insert#set_line_offset 0 in + let current_line_spaces = get_nb_space current_line_start in + if input_buffer#delete_interactive + ~start:current_line_start + ~stop:(current_line_start#forward_chars current_line_spaces) + () + then + let current_line_start = self#get_insert#set_line_offset 0 in + input_buffer#insert + ~iter:current_line_start + (String.make previous_line_spaces ' ') + end - method show_pm_goal = - proof_buffer#insert - (Printf.sprintf " *** Declarative Mode ***\n"); - try - 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"); - 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)) - my_mark; - ignore (proof_view#scroll_to_mark my_mark) - with Not_found -> + method show_pm_goal = + proof_buffer#insert + (Printf.sprintf " *** Declarative Mode ***\n"); + try + 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"); + 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)) + my_mark; + ignore (proof_view#scroll_to_mark my_mark) + with Not_found -> match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with - Some endc -> - proof_buffer#insert - ("Subproof completed, now type "^endc^".") - | None -> - proof_buffer#insert "Proof completed." + Some endc -> + proof_buffer#insert + ("Subproof completed, now type "^endc^".") + | None -> + proof_buffer#insert "Proof completed." + - method show_goals = - try - proof_view#buffer#set_text ""; - match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ()) - | Decl_mode.Mode_tactic -> - begin - let s = Coq.get_current_goals () in - match s with - | [] -> proof_buffer#insert (Coq.print_no_goal ()) - | (hyps,concl)::r -> - let goal_nb = List.length s in - proof_buffer#insert - (Printf.sprintf "%d subgoal%s\n" - goal_nb - (if goal_nb<=1 then "" else "s")); - List.iter - (fun ((_,_,_,(s,_)) as _hyp) -> - proof_buffer#insert (s^"\n")) - hyps; - proof_buffer#insert - (String.make 38 '_' ^ "(1/"^ - (string_of_int goal_nb)^ - ")\n") ; - let _,_,_,sconcl = concl in - proof_buffer#insert sconcl; - proof_buffer#insert "\n"; - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) - my_mark; - proof_buffer#insert "\n\n"; - let i = ref 1 in - List.iter - (function (_,(_,_,_,concl)) -> - incr i; - proof_buffer#insert - (String.make 38 '_' ^"("^ - (string_of_int !i)^ - "/"^ - (string_of_int goal_nb)^ - ")\n"); - proof_buffer#insert concl; - proof_buffer#insert "\n\n"; - ) - r; - ignore (proof_view#scroll_to_mark my_mark) - end - | Decl_mode.Mode_proof -> - self#show_pm_goal - with e -> - prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) - - val mutable full_goal_done = true - method show_goals_full = + method show_goals_full = if not full_goal_done then begin - try - proof_view#buffer#set_text ""; - match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> - proof_buffer#insert (Coq.print_no_goal ()) - | Decl_mode.Mode_tactic -> - begin - match Coq.get_current_goals () with - [] -> Util.anomaly "show_goals_full" - | ((hyps,concl)::r) as s -> - let last_shown_area = - proof_buffer#create_tag [`BACKGROUND "light green"] - in - let goal_nb = List.length s in - proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" - goal_nb - (if goal_nb<=1 then "" else "s")); - let coq_menu commands = - let tag = proof_buffer#create_tag [] - in - ignore - (tag#connect#event ~callback: - (fun ~origin ev it -> - begin match GdkEvent.get_type ev with - | `BUTTON_PRESS -> - let ev = (GdkEvent.Button.cast ev) in - if (GdkEvent.Button.button ev) = 3 - then begin - let loc_menu = GMenu.menu () in - let factory = - new GMenu.factory loc_menu in - let add_coq_command (cp,ip) = - ignore - (factory#add_item cp - ~callback: - (fun () -> ignore - (self#insert_this_phrase_on_success - true - true - false - ("progress "^ip^"\n") - (ip^"\n")) - ) - ) - in - List.iter add_coq_command commands; - loc_menu#popup - ~button:3 - ~time:(GdkEvent.Button.time ev); - end - | `MOTION_NOTIFY -> - proof_buffer#remove_tag - ~start:proof_buffer#start_iter - ~stop:proof_buffer#end_iter - last_shown_area; - prerr_endline "Before find_tag_limits"; - - let s,e = find_tag_limits tag - (new GText.iter it) - in - prerr_endline "After find_tag_limits"; - proof_buffer#apply_tag - ~start:s - ~stop:e - last_shown_area; - - prerr_endline "Applied tag"; - () - | _ -> () - end;false - ) - ); - tag - in - List.iter - (fun ((_,_,_,(s,_)) as hyp) -> - let tag = coq_menu (hyp_menu hyp) in - proof_buffer#insert ~tags:[tag] (s^"\n")) - hyps; - proof_buffer#insert - (String.make 38 '_' ^"(1/"^ - (string_of_int goal_nb)^ - ")\n") - ; - let tag = coq_menu (concl_menu concl) in - let _,_,_,sconcl = concl in - proof_buffer#insert ~tags:[tag] sconcl; - proof_buffer#insert "\n"; - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; - proof_buffer#insert "\n\n"; - let i = ref 1 in - List.iter - (function (_,(_,_,_,concl)) -> - incr i; - proof_buffer#insert - (String.make 38 '_' ^"("^ - (string_of_int !i)^ - "/"^ - (string_of_int goal_nb)^ - ")\n"); - proof_buffer#insert concl; - proof_buffer#insert "\n\n"; - ) - r; - ignore (proof_view#scroll_to_mark my_mark) ; - full_goal_done <- true - end - | Decl_mode.Mode_proof -> - self#show_pm_goal - with e -> prerr_endline (Printexc.to_string e) + try + proof_buffer#set_text ""; + match Decl_mode.get_current_mode () with + Decl_mode.Mode_none -> () + | Decl_mode.Mode_tactic -> + begin + match Coq.get_current_goals () with + [] -> proof_buffer#insert (Coq.print_no_goal()) + | ((hyps,concl)::r) as s -> + let last_shown_area = Tags.Proof.highlight + in + let goal_nb = List.length s in + proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" + goal_nb + (if goal_nb<=1 then "" else "s")); + let coq_menu commands = + let tag = proof_buffer#create_tag [] + in + ignore + (tag#connect#event ~callback: + (fun ~origin ev it -> + match GdkEvent.get_type ev with + | `BUTTON_PRESS -> + let ev = (GdkEvent.Button.cast ev) in + if (GdkEvent.Button.button ev) = 3 + then ( + let loc_menu = GMenu.menu () in + let factory = + new GMenu.factory loc_menu in + let add_coq_command (cp,ip) = + ignore + (factory#add_item cp + ~callback: + (fun () -> ignore + (self#insert_this_phrase_on_success + true + true + false + ("progress "^ip^"\n") + (ip^"\n")) + ) + ) + in + List.iter add_coq_command commands; + loc_menu#popup + ~button:3 + ~time:(GdkEvent.Button.time ev); + true) + else false + | `MOTION_NOTIFY -> + proof_buffer#remove_tag + ~start:proof_buffer#start_iter + ~stop:proof_buffer#end_iter + last_shown_area; + prerr_endline "Before find_tag_limits"; + + let s,e = find_tag_limits tag + (new GText.iter it) + in + prerr_endline "After find_tag_limits"; + proof_buffer#apply_tag + ~start:s + ~stop:e + last_shown_area; + + prerr_endline "Applied tag"; + false + | _ -> + false + ) + ); + tag + in + List.iter + (fun ((_,_,_,(s,_)) as hyp) -> + let tag = coq_menu (hyp_menu hyp) in + proof_buffer#insert ~tags:[tag] (s^"\n")) + hyps; + proof_buffer#insert + (String.make 38 '_' ^"(1/"^ + (string_of_int goal_nb)^ + ")\n") + ; + let tag = coq_menu (concl_menu concl) in + let _,_,_,sconcl = concl in + proof_buffer#insert ~tags:[tag] sconcl; + proof_buffer#insert "\n"; + let my_mark = `NAME "end_of_conclusion" in + proof_buffer#move_mark + ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; + proof_buffer#insert "\n\n"; + let i = ref 1 in + List.iter + (function (_,(_,_,_,concl)) -> + incr i; + proof_buffer#insert + (String.make 38 '_' ^"("^ + (string_of_int !i)^ + "/"^ + (string_of_int goal_nb)^ + ")\n"); + proof_buffer#insert concl; + proof_buffer#insert "\n\n"; + ) + r; + ignore (proof_view#scroll_to_mark my_mark) ; + full_goal_done <- true + end + | Decl_mode.Mode_proof -> + self#show_pm_goal + with e -> prerr_endline (Printexc.to_string e) end - + + method show_goals = self#show_goals_full + + method send_to_coq verbosely replace phrase show_output show_error localize = let display_output msg = self#insert_message (if show_output then msg else "") in let display_error e = let (s,loc) = Coq.process_exn e in - assert (Glib.Utf8.validate s); - self#insert_message s; - message_view#misc#draw None; - if localize then - (match Option.map Util.unloc loc with - | None -> () - | Some (start,stop) -> - let convert_pos = byte_offset_to_char_offset phrase in - let start = convert_pos start in - let stop = convert_pos stop in - let i = self#get_start_of_input in - let starti = i#forward_chars start in - let stopi = i#forward_chars stop in - input_buffer#apply_tag_by_name "error" - ~start:starti - ~stop:stopi; - input_buffer#place_cursor starti) in - try - full_goal_done <- false; - prerr_endline "Send_to_coq starting now"; - Decl_mode.clear_daimon_flag (); - if replace then begin - let r,info = Coq.interp_and_replace ("info " ^ phrase) in - let complete = not (Decl_mode.get_daimon_flag ()) in - let msg = read_stdout () in - sync display_output msg; - Some (complete,r) - end else begin - let r = Coq.interp verbosely phrase in - let complete = not (Decl_mode.get_daimon_flag ()) in - let msg = read_stdout () in - sync display_output msg; - Some (complete,r) - end - with e -> - if show_error then sync display_error e; - None - - method find_phrase_starting_at (start:GText.iter) = - prerr_endline "find_phrase_starting_at starting now"; - let trash_bytes = ref "" in - let end_iter = start#copy in - let lexbuf_function s count = - let i = ref 0 in - let n_trash = String.length !trash_bytes in - String.blit !trash_bytes 0 s 0 n_trash; - i := n_trash; - try - while !i <= count - 1 do - let c = end_iter#char in - if c = 0 then raise (Stop !i); - let c' = Glib.Utf8.from_unichar c in - let n = String.length c' in - if (n<=0) then exit (-2); - if n > count - !i then - begin - let ri = count - !i in - String.blit c' 0 s !i ri; - trash_bytes := String.sub c' ri (n-ri); - i := count ; - end else begin - String.blit c' 0 s !i n; - i:= !i + n - end; - if not end_iter#nocopy#forward_char then - raise (Stop !i) - done; - count - with Stop x -> - x - in + assert (Glib.Utf8.validate s); + self#insert_message s; + message_view#misc#draw None; + if localize then + (match Option.map Util.unloc loc with + | None -> () + | Some (start,stop) -> + let convert_pos = byte_offset_to_char_offset phrase in + let start = convert_pos start in + let stop = convert_pos stop in + let i = self#get_start_of_input in + let starti = i#forward_chars start in + let stopi = i#forward_chars stop in + input_buffer#apply_tag Tags.Script.error + ~start:starti + ~stop:stopi; + input_buffer#place_cursor starti) in try - trash_bytes := ""; - let _ = Find_phrase.get (Lexing.from_function lexbuf_function) - in - end_iter#nocopy#set_offset (start#offset + !Find_phrase.length); - Some (start,end_iter) - with - (* - | Find_phrase.EOF s -> - (* Phrase is at the end of the buffer*) - let si = start#offset in - let ei = si + !Find_phrase.length in - end_iter#nocopy#set_offset (ei - 1); - input_buffer#insert ~iter:end_iter "\n"; - Some (input_buffer#get_iter (`OFFSET si), - input_buffer#get_iter (`OFFSET ei)) - *) - | _ -> None - - method complete_at_offset (offset:int) = + full_goal_done <- false; + prerr_endline "Send_to_coq starting now"; + Decl_mode.clear_daimon_flag (); + if replace then begin + let r,info = Coq.interp_and_replace ("info " ^ phrase) in + let is_complete = not (Decl_mode.get_daimon_flag ()) in + let msg = read_stdout () in + sync display_output msg; + Some (is_complete,r) + end else begin + let r = Coq.interp verbosely phrase in + let is_complete = not (Decl_mode.get_daimon_flag ()) in + let msg = read_stdout () in + sync display_output msg; + Some (is_complete,r) + end + with e -> + if show_error then sync display_error e; + None + + method find_phrase_starting_at (start:GText.iter) = + try + let start = grab_safe_sentence_start start self#get_start_of_input in + let stop = grab_sentence_end_from start in + if stop#backward_char#has_tag Tags.Script.lax_end then + Some (start,stop) + else + None + with Not_found -> None + + method complete_at_offset (offset:int) = prerr_endline ("Completion at offset : " ^ string_of_int offset); let it () = input_buffer#get_iter (`OFFSET offset) in let iit = it () in let start = find_word_start iit in - if ends_word iit then - let w = input_buffer#get_text - ~start - ~stop:iit - () - in - if String.length w <> 0 then begin - prerr_endline ("Completion of prefix : '" ^ w^"'"); - match complete input_buffer w start#offset with - | None -> false - | Some (ss,start,stop) -> - let completion = input_buffer#get_text ~start ~stop () in - ignore (input_buffer#delete_selection ()); - ignore (input_buffer#insert_interactive completion); - input_buffer#move_mark `SEL_BOUND (it())#backward_char; - true - end else false - else false - - - method process_next_phrase verbosely display_goals do_highlight = + if ends_word iit then + let w = input_buffer#get_text + ~start + ~stop:iit + () + in + if String.length w <> 0 then begin + prerr_endline ("Completion of prefix : '" ^ w^"'"); + match complete input_buffer w start#offset with + | None -> false + | Some (ss,start,stop) -> + let completion = input_buffer#get_text ~start ~stop () in + ignore (input_buffer#delete_selection ()); + ignore (input_buffer#insert_interactive completion); + input_buffer#move_mark `SEL_BOUND (it())#backward_char; + true + end else false + else false + + method process_next_phrase verbosely display_goals do_highlight = let get_next_phrase () = self#clear_message; prerr_endline "process_next_phrase starting now"; if do_highlight then begin - !push_info "Coq is computing"; - input_view#set_editable false; - end; - match self#find_phrase_starting_at self#get_start_of_input with - | None -> - if do_highlight then begin - input_view#set_editable true; - !pop_info (); - end; + push_info "Coq is computing"; + input_view#set_editable false; + end; + match self#find_phrase_starting_at self#get_start_of_input with + | None -> + if do_highlight then begin + input_view#set_editable true; + pop_info (); + end; None - | Some(start,stop) -> - prerr_endline "process_next_phrase : to_process highlight"; - if do_highlight then begin - input_buffer#apply_tag_by_name ~start ~stop "to_process"; - prerr_endline "process_next_phrase : to_process applied"; - end; - prerr_endline "process_next_phrase : getting phrase"; + | Some(start,stop) -> + prerr_endline "process_next_phrase : to_process highlight"; + if do_highlight then begin + input_buffer#apply_tag Tags.Script.to_process ~start ~stop; + prerr_endline "process_next_phrase : to_process applied"; + end; + prerr_endline "process_next_phrase : getting phrase"; Some((start,stop),start#get_slice ~stop) in let remove_tag (start,stop) = if do_highlight then begin - input_buffer#remove_tag_by_name ~start ~stop "to_process" ; - input_view#set_editable true; - !pop_info (); - end in - 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 - (if complete then "processed" else "unjustified") ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - begin - b#place_cursor stop; - self#recenter_insert - 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 - reset_info - start_of_phrase_mark - end_of_phrase_mark ast; - if display_goals then self#show_goals; - remove_tag (start,stop) in - begin - match sync get_next_phrase () with - None -> false - | Some (loc,phrase) -> + input_buffer#remove_tag Tags.Script.to_process ~start ~stop; + input_view#set_editable true; + pop_info (); + end in + let mark_processed reset_info is_complete (start,stop) = + let b = input_buffer in + b#move_mark ~where:stop (`NAME "start_of_input"); + b#apply_tag + (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + begin + b#place_cursor stop; + self#recenter_insert + end; + let ide_payload = { start = `MARK (b#create_mark start); + stop = `MARK (b#create_mark stop); } in + push_phrase + cmd_stack + reset_info + ide_payload; + if display_goals then self#show_goals; + remove_tag (start,stop) in + begin + match sync get_next_phrase () with + None -> false + | Some (loc,phrase) -> (match self#send_to_coq verbosely false phrase true true true with - | 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 reset_info complete ast = + | Some (is_complete,reset_info) -> + sync (mark_processed reset_info is_complete) loc; true + | None -> sync remove_tag loc; false) + end + + method insert_this_phrase_on_success + show_output show_msg localize coqphrase insertphrase = + let mark_processed reset_info is_complete = let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop insertphrase - else input_buffer#insert ~iter:stop ("\n"^insertphrase); - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name - (if complete then "processed" else "unjustified") ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - 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 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 - | [] -> - (match self#send_to_coq "Save.\n" true true true with - | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop "Save.\n" - else input_buffer#insert ~iter:stop "\nSave.\n"; - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME"start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - 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 - 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,(reset_info,ast)) -> - sync (mark_processed reset_info complete) ast; true - | None -> - sync - (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) - (); - false + if stop#starts_line then + input_buffer#insert ~iter:stop insertphrase + else input_buffer#insert ~iter:stop ("\n"^insertphrase); + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME "start_of_input"); + input_buffer#apply_tag + (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let ide_payload = { start = `MARK (input_buffer#create_mark start); + stop = `MARK (input_buffer#create_mark stop); } in + push_phrase cmd_stack reset_info ide_payload; + self#show_goals; + (*Auto insert save on success... + try (match Coq.get_current_goals () with + | [] -> + (match self#send_to_coq "Save.\n" true true true with + | Some ast -> + begin + let stop = self#get_start_of_input in + if stop#starts_line then + input_buffer#insert ~iter:stop "Save.\n" + else input_buffer#insert ~iter:stop "\nSave.\n"; + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME"start_of_input"); + input_buffer#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + 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 + 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 (is_complete,reset_info) -> + sync (mark_processed reset_info) is_complete; true + | None -> + sync + (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) + (); + false method process_until_iter_or_error stop = let stop' = `OFFSET stop#offset in let start = self#get_start_of_input#copy in let start' = `OFFSET start#offset in sync (fun _ -> - input_buffer#apply_tag_by_name ~start ~stop "to_process"; - input_view#set_editable false) (); - !push_info "Coq is computing"; + input_buffer#apply_tag Tags.Script.to_process ~start ~stop; + input_view#set_editable false) (); + push_info "Coq is computing"; let get_current () = - if !current.stop_before then + if !current.stop_before then match self#find_phrase_starting_at self#get_start_of_input with | None -> self#get_start_of_input | Some (_, stop2) -> stop2 - else begin - self#get_start_of_input - end - in - (try - while ((stop#compare (get_current())>=0) - && (self#process_next_phrase false false false)) - do Util.check_for_interrupt () done - with Sys.Break -> - prerr_endline "Interrupted during process_until_iter_or_error"); - sync (fun _ -> - self#show_goals; - (* Start and stop might be invalid if an eol was added at eof *) - let start = input_buffer#get_iter start' in - let stop = input_buffer#get_iter stop' in - input_buffer#remove_tag_by_name ~start ~stop "to_process" ; - input_view#set_editable true) (); - !pop_info() - - method process_until_end_or_error = + else begin + self#get_start_of_input + end + in + (try + while ((stop#compare (get_current())>=0) + && (self#process_next_phrase false false false)) + do Util.check_for_interrupt () done + with Sys.Break -> + prerr_endline "Interrupted during process_until_iter_or_error"); + sync (fun _ -> + self#show_goals; + (* Start and stop might be invalid if an eol was added at eof *) + let start = input_buffer#get_iter start' in + let stop = input_buffer#get_iter stop' in + input_buffer#remove_tag Tags.Script.to_process ~start ~stop; + input_view#set_editable true) (); + pop_info() + + method process_until_end_or_error = self#process_until_iter_or_error input_buffer#end_iter method reset_initial = sync (fun _ -> - Stack.iter - (function inf -> - let start = input_buffer#get_iter_at_mark inf.start in - let stop = input_buffer#get_iter_at_mark inf.stop in - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - input_buffer#remove_tag_by_name "processed" ~start ~stop; - input_buffer#remove_tag_by_name "unjustified" ~start ~stop; - input_buffer#delete_mark inf.start; - input_buffer#delete_mark inf.stop; - ) - processed_stack; - Stack.clear processed_stack; - self#clear_message)(); + Stack.iter + (function (inf,_) -> + let start = input_buffer#get_iter_at_mark inf.start in + let stop = input_buffer#get_iter_at_mark inf.stop in + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + input_buffer#remove_tag Tags.Script.processed ~start ~stop; + input_buffer#remove_tag Tags.Script.unjustified ~start ~stop; + input_buffer#delete_mark inf.start; + input_buffer#delete_mark inf.stop; + ) + cmd_stack; + Stack.clear cmd_stack; + 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."; (* pop Coq commands until we reach iterator [i] *) - let rec pop_commands done_smthg undos = - if is_empty () then - done_smthg, undos + let rec pop_cmds popped = + if Stack.is_empty cmd_stack then + popped else - let t = top () in - if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then + let (ide,coq) = Stack.pop cmd_stack in + if i#compare (input_buffer#get_iter_at_mark ide.stop) < 0 then begin - prerr_endline "Popped top command"; - pop_commands true (pop_command undos t) - end + prerr_endline "popped command"; + pop_cmds (coq::popped) + end else - done_smthg, undos + begin + Stack.push (ide,coq) cmd_stack; + popped + end in - let undos = (0,0,NoBacktrack,0,undo_info()) in - let done_smthg, undos = pop_commands false undos in + let seq = List.rev (pop_cmds []) in prerr_endline "Popped commands"; - if done_smthg then - begin - try - apply_undos undos; + if 0 < List.length seq then + begin + try + rewind seq cmd_stack; sync (fun _ -> - let start = - if is_empty () then input_buffer#start_iter - else input_buffer#get_iter_at_mark (top ()).stop in - prerr_endline "Removing (long) processed tag..."; - input_buffer#remove_tag_by_name - ~start - ~stop:self#get_start_of_input - "processed"; - input_buffer#remove_tag_by_name - ~start - ~stop:self#get_start_of_input - "unjustified"; - prerr_endline "Moving (long) start_of_input..."; - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - self#show_goals; - clear_stdout (); - self#clear_message) + let start = + if Stack.is_empty cmd_stack then input_buffer#start_iter + else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in + prerr_endline "Removing (long) processed tag..."; + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop:self#get_start_of_input; + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop:self#get_start_of_input; + prerr_endline "Moving (long) start_of_input..."; + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + full_goal_done <- false; + self#show_goals; + clear_stdout (); + self#clear_message) (); - with _ -> - !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. -Please restart and report NOW."; - end - else prerr_endline "backtrack_to : discarded (...)" - - method backtrack_to i = - if Mutex.try_lock coq_may_stop then - (!push_info "Undoing..."; + with _ -> + push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. + Please restart and report NOW."; + end + else prerr_endline "backtrack_to : discarded (...)" + + 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; - !pop_info ()) + pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" method go_to_insert = @@ -1411,405 +1172,278 @@ Please restart and report NOW."; else self#backtrack_to point method undo_last_step = - if Mutex.try_lock coq_may_stop then - (!push_info "Undoing last step..."; + if Mutex.try_lock coq_may_stop then + (push_info "Undoing last step..."; (try - let last_command = top () in - let start = input_buffer#get_iter_at_mark last_command.start in - let update_input () = - prerr_endline "Removing processed tag..."; - input_buffer#remove_tag_by_name - ~start - ~stop:(input_buffer#get_iter_at_mark last_command.stop) - "processed"; - input_buffer#remove_tag_by_name - ~start - ~stop:(input_buffer#get_iter_at_mark last_command.stop) - "unjustified"; - prerr_endline "Moving start_of_input"; - input_buffer#move_mark - ~where:start - (`NAME "start_of_input"); - input_buffer#place_cursor start; - self#recenter_insert; - self#show_goals; - self#clear_message - in - 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"*)() + let (ide_ri,_) = Stack.top cmd_stack in + let start = input_buffer#get_iter_at_mark ide_ri.start in + let update_input () = + prerr_endline "Removing processed tag..."; + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop:(input_buffer#get_iter_at_mark ide_ri.stop); + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop:(input_buffer#get_iter_at_mark ide_ri.stop); + prerr_endline "Moving start_of_input"; + input_buffer#move_mark + ~where:start + (`NAME "start_of_input"); + input_buffer#place_cursor start; + self#recenter_insert; + full_goal_done <- false; + self#show_goals; + self#clear_message + in + let _,coq = Stack.pop cmd_stack in + rewind [coq] cmd_stack; + sync update_input () + with + | Stack.Empty -> (* flash_info "Nothing to Undo"*)() ); - !pop_info (); + pop_info (); Mutex.unlock coq_may_stop) else prerr_endline "undo_last_step discarded" - - method blaster () = - - ignore (Thread.create - (fun () -> - prerr_endline "Blaster called"; - let c = Blaster_window.present_blaster_window () in - if Mutex.try_lock c#lock then begin - c#clear (); - Decl_mode.check_not_proof_mode "No blaster in Proof mode"; - let current_gls = try get_current_goals () with _ -> [] in - - let set_goal i (s,t) = - let gnb = string_of_int i in - let s = gnb ^":"^s in - let t' = gnb ^": progress "^t in - let t'' = gnb ^": "^t in - c#set - ("Goal "^gnb) - s - (fun () -> try_interptac t') - (sync(fun () -> self#insert_command t'' t'')) - in - let set_current_goal (s,t) = - c#set - "Goal 1" - s - (fun () -> try_interptac ("progress "^t)) - (sync(fun () -> self#insert_command t t)) - in - begin match current_gls with - | [] -> () - | (hyp_l,current_gl)::r -> - List.iter set_current_goal (concl_menu current_gl); - List.iter - (fun hyp -> - List.iter set_current_goal (hyp_menu hyp)) - hyp_l; - let i = ref 2 in - List.iter - (fun (hyp_l,gl) -> - List.iter (set_goal !i) (concl_menu gl); - incr i) - r - end; - let _ = c#blaster () in - Mutex.unlock c#lock - end else prerr_endline "Blaster discarded") - ()) - - method insert_command cp ip = + + method insert_command cp ip = async(fun _ -> self#clear_message)(); ignore (self#insert_this_phrase_on_success true false false cp ip) method tactic_wizard l = async(fun _ -> self#clear_message)(); - ignore - (List.exists - (fun p -> - self#insert_this_phrase_on_success true false false - ("progress "^p^".\n") (p^".\n")) l) - - method active_keypress_handler k = + ignore + (List.exists + (fun p -> + self#insert_this_phrase_on_success true false false + ("progress "^p^".\n") (p^".\n")) l) + + method active_keypress_handler k = let state = GdkEvent.Key.state k in begin - match state with - | l when List.mem `MOD1 l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._Return=k - then ignore( - if (input_buffer#insert_interactive "\n") then - begin - let i= self#get_insert#backward_word_start in - prerr_endline "active_kp_hf: Placing cursor"; - self#process_until_iter_or_error i - end); - true - | l when List.mem `CONTROL l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._Break=k - then break (); - false - | l -> - if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin - prerr_endline "active_kp_handler for Tab"; - self#indent_current_line; - true - end else false + match state with + | l when List.mem `MOD1 l -> + let k = GdkEvent.Key.keyval k in + if GdkKeysyms._Return=k + then ignore( + if (input_buffer#insert_interactive "\n") then + begin + let i= self#get_insert#backward_word_start in + prerr_endline "active_kp_hf: Placing cursor"; + self#process_until_iter_or_error i + end); + true + | l when List.mem `CONTROL l -> + let k = GdkEvent.Key.keyval k in + if GdkKeysyms._Break=k + then break (); + false + | l -> + if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin + prerr_endline "active_kp_handler for Tab"; + self#indent_current_line; + true + end else false end - method disconnected_keypress_handler k = + + + method disconnected_keypress_handler k = match GdkEvent.Key.state k with - | l when List.mem `CONTROL l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._c=k - then break (); - false + | l when List.mem `CONTROL l -> + let k = GdkEvent.Key.keyval k in + if GdkKeysyms._c=k + then break (); + false | l -> false - + val mutable deact_id = None val mutable act_id = None - method deactivate () = + method deactivate () = is_active <- false; - (match act_id with None -> () + (match act_id with None -> () | Some id -> - reset_initial (); - input_view#misc#disconnect id; - prerr_endline "DISCONNECTED old active : "; - print_id id; - ); - deact_id <- Some - (input_view#event#connect#key_press self#disconnected_keypress_handler); + reset_initial (); + input_view#misc#disconnect id; + prerr_endline "DISCONNECTED old active : "; + print_id id; + )(*; + deact_id <- Some + (input_view#event#connect#key_press self#disconnected_keypress_handler); prerr_endline "CONNECTED inactive : "; - print_id (Option.get deact_id) + print_id (Option.get deact_id)*) + (* XXX *) method activate () = - is_active <- true; - (match deact_id with None -> () + is_active <- true;(* + (match deact_id with None -> () | Some id -> input_view#misc#disconnect id; - prerr_endline "DISCONNECTED old inactive : "; - print_id id - ); - act_id <- Some - (input_view#event#connect#key_press self#active_keypress_handler); + prerr_endline "DISCONNECTED old inactive : "; + print_id id + );*) + act_id <- Some + (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; print_id (Option.get act_id); - match - (Option.get ((Vector.get input_views index).analyzed_view)) #filename + match + filename with | None -> () | Some f -> let dir = Filename.dirname f in - if not (is_in_loadpath dir) then - begin - ignore (Coq.interp false - (Printf.sprintf "Add LoadPath \"%s\". " dir)) - end - - method electric_handler = + if not (is_in_loadpath dir) then + begin + ignore (Coq.interp false + (Printf.sprintf "Add LoadPath \"%s\". " dir)) + end + + method electric_handler = input_buffer#connect#insert_text ~callback: - (fun it x -> - begin try - if last_index then begin - last_array.(0)<-x; - if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found - end else begin - last_array.(1)<-x; - if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found - end - with Found -> - begin - ignore (self#process_next_phrase false true true) - end; - end; - last_index <- not last_index;) + (fun it x -> + begin try + if last_index then begin + last_array.(0)<-x; + if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found + end else begin + last_array.(1)<-x; + if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found + end + with Found -> + begin + ignore (self#process_next_phrase false true true) + end; + end; + last_index <- not last_index;) method private electric_paren tag = let oparen_code = Glib.Utf8.to_unichar "(" (ref 0) in let cparen_code = Glib.Utf8.to_unichar ")" (ref 0) in ignore (input_buffer#connect#insert_text ~callback: - (fun it x -> - input_buffer#remove_tag - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter - tag; - if x = "" then () else - match x.[String.length x - 1] with - | ')' -> - let hit = self#get_insert in - let count = ref 0 in - if hit#nocopy#backward_find_char - (fun c -> - if c = oparen_code && !count = 0 then true - else if c = cparen_code then - (incr count;false) - else if c = oparen_code then - (decr count;false) - else false - ) - then - begin - prerr_endline "Found matching parenthesis"; - input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char - end - else () - | _ -> ()) - ) + (fun it x -> + input_buffer#remove_tag + ~start:input_buffer#start_iter + ~stop:input_buffer#end_iter + tag; + if x = "" then () else + match x.[String.length x - 1] with + | ')' -> + let hit = self#get_insert in + let count = ref 0 in + if hit#nocopy#backward_find_char + (fun c -> + if c = oparen_code && !count = 0 then true + else if c = cparen_code then + (incr count;false) + else if c = oparen_code then + (decr count;false) + else false + ) + then + begin + prerr_endline "Found matching parenthesis"; + input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char + end + else () + | _ -> ()) + ) + + method help_for_keyword () = - method help_for_keyword () = - browse_keyword (self#insert_message) (get_current_word ()) - initializer + initializer ignore (message_buffer#connect#insert_text - ~callback:(fun it s -> ignore - (message_view#scroll_to_mark - ~use_align:false - ~within_margin:0.49 - `INSERT))); + ~callback:(fun it s -> ignore + (message_view#scroll_to_mark + ~use_align:false + ~within_margin:0.49 + `INSERT))); ignore (input_buffer#connect#insert_text - ~callback:(fun it s -> - if (it#compare self#get_start_of_input)<0 - then GtkSignal.stop_emit (); - if String.length s > 1 then - (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it))); + ~callback:(fun it s -> + if (it#compare self#get_start_of_input)<0 + then GtkSignal.stop_emit (); + if String.length s > 1 then + (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it))); ignore (input_buffer#connect#after#apply_tag - ~callback:(fun tag ~start ~stop -> - if (start#compare self#get_start_of_input)>=0 - then - begin - input_buffer#remove_tag_by_name - ~start - ~stop - "processed"; - input_buffer#remove_tag_by_name - ~start - ~stop - "unjustified" - end - ) - ); + ~callback:(fun tag ~start ~stop -> + if (start#compare self#get_start_of_input)>=0 + then + begin + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop; + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop + end + ) + ); ignore (input_buffer#connect#after#insert_text - ~callback:(fun it s -> - if auto_complete_on && - String.length s = 1 && s <> " " && s <> "\n" - then - let v = Option.get (get_current_view ()).analyzed_view - in - let has_completed = - v#complete_at_offset - ((v#view#buffer#get_iter `SEL_BOUND)#offset) - in - if has_completed then - input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char; - - - ) - ); - ignore (input_buffer#connect#modified_changed - ~callback: - (fun () -> - if input_buffer#modified then - set_tab_image index - ~icon:(match (Option.get (current_all.analyzed_view))#filename with - | None -> `SAVE_AS - | Some _ -> `SAVE - ) - else set_tab_image index ~icon:`YES; - )); + ~callback:(fun it s -> + if auto_complete_on && + String.length s = 1 && s <> " " && s <> "\n" + then + let v = session_notebook#current_term.analyzed_view + in + let has_completed = + v#complete_at_offset + ((input_view#buffer#get_iter `SEL_BOUND)#offset) + in + if has_completed then + input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char; + + + ) + ); ignore (input_buffer#connect#changed - ~callback:(fun () -> - last_modification_time <- Unix.time (); - let r = input_view#visible_rect in - let stop = - input_view#get_iter_at_location - ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r) - ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r) - in - input_buffer#remove_tag_by_name - ~start:self#get_start_of_input - ~stop - "error"; - Highlight.highlight_around_current_line - input_buffer - ) - ); - ignore (input_buffer#add_selection_clipboard (cb())); - let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in - self#electric_paren paren_highlight_tag; - ignore (input_buffer#connect#after#mark_set - ~callback:(fun it (m:Gtk.text_mark) -> - !set_location - (Printf.sprintf - "Line: %5d Char: %3d" (self#get_insert#line + 1) - (self#get_insert#line_offset + 1)); - match GtkText.Mark.get_name m with - | Some "insert" -> - input_buffer#remove_tag - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter - paren_highlight_tag; - | Some s -> - prerr_endline (s^" moved") - | None -> () ) - ); + ~callback:(fun () -> + last_modification_time <- Unix.time (); + let r = input_view#visible_rect in + let stop = + input_view#get_iter_at_location + ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r) + ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r) + in + input_buffer#remove_tag + Tags.Script.error + ~start:self#get_start_of_input + ~stop; + tag_on_insert input_buffer + ) + ); + ignore (input_buffer#add_selection_clipboard cb); + ignore (proof_buffer#add_selection_clipboard cb); + ignore (message_buffer#add_selection_clipboard cb); + self#electric_paren Tags.Script.paren; + ignore (input_buffer#connect#after#mark_set + ~callback:(fun it (m:Gtk.text_mark) -> + !set_location + (Printf.sprintf + "Line: %5d Char: %3d" (self#get_insert#line + 1) + (self#get_insert#line_offset + 1)); + match GtkText.Mark.get_name m with + | Some "insert" -> + input_buffer#remove_tag + ~start:input_buffer#start_iter + ~stop:input_buffer#end_iter + Tags.Script.paren; + | Some s -> + prerr_endline (s^" moved") + | None -> () ) + ); ignore (input_buffer#connect#insert_text - (fun it s -> - prerr_endline "Should recenter ?"; - if String.contains s '\n' then begin - prerr_endline "Should recenter : yes"; - self#recenter_insert - end)) + (fun it s -> + prerr_endline "Should recenter ?"; + if String.contains s '\n' then begin + prerr_endline "Should recenter : yes"; + self#recenter_insert + end)); end -let create_input_tab filename = - let b = GText.buffer () in - let _ = GMisc.label () in - let v_box = GPack.hbox ~homogeneous:false () in - let _ = GMisc.image ~packing:v_box#pack () in - let _ = GMisc.label ~text:filename ~packing:v_box#pack () in - let appendp x = ignore ((notebook ())#append_page - ~tab_label:v_box#coerce x) in - let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:appendp () - in - let sw1 = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:fr1#add () - in - let tv1 = Undo.undoable_view ~buffer:b ~packing:(sw1#add) () in - prerr_endline ("Language: "^ b#start_iter#language); - tv1#misc#set_name "ScriptWindow"; - let _ = tv1#set_editable true in - let _ = tv1#set_wrap_mode `NONE in - b#place_cursor ~where:(b#start_iter); - ignore (tv1#event#connect#button_press ~callback: - (fun ev -> GdkEvent.Button.button ev = 3)); - (* ignore (tv1#event#connect#button_press ~callback: - (fun ev -> - if (GdkEvent.Button.button ev=2) then - (try - prerr_endline "Paste invoked"; - GtkSignal.emit_unit - (get_current_view()).view#as_view - GtkText.View.Signals.paste_clipboard; - true - with _ -> false) - else false - ));*) - tv1#misc#grab_focus (); - ignore (tv1#buffer#create_mark - ~name:"start_of_input" - tv1#buffer#start_iter); - ignore (tv1#buffer#create_tag - ~name:"kwd" - [`FOREGROUND "blue"]); - ignore (tv1#buffer#create_tag - ~name:"decl" - [`FOREGROUND "orange red"]); - ignore (tv1#buffer#create_tag - ~name:"comment" - [`FOREGROUND "brown"]); - ignore (tv1#buffer#create_tag - ~name:"reserved" - [`FOREGROUND "dark red"]); - ignore (tv1#buffer#create_tag - ~name:"error" - [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]); - ignore (tv1#buffer#create_tag - ~name:"to_process" - [`BACKGROUND "light blue" ;`EDITABLE false]); - ignore (tv1#buffer#create_tag - ~name:"processed" - [`BACKGROUND "light green" ;`EDITABLE false]); - ignore (tv1#buffer#create_tag (* Proof mode *) - ~name:"unjustified" - [`UNDERLINE `SINGLE ; `FOREGROUND "red"; - `BACKGROUND "gold" ;`EDITABLE false]); - ignore (tv1#buffer#create_tag - ~name:"found" - [`BACKGROUND "blue"; `FOREGROUND "white"]); - tv1 - - let last_make = ref "";; let last_make_index = ref 0;; let search_compile_error_regexp = @@ -1823,20 +1457,228 @@ let search_next_error () = and b = int_of_string (Str.matched_group 3 !last_make) and e = int_of_string (Str.matched_group 4 !last_make) and msg_index = Str.match_beginning () - in - last_make_index := Str.group_end 4; + in + last_make_index := Str.group_end 4; (f,l,b,e, String.sub !last_make msg_index (String.length !last_make - msg_index)) -let main files = + + +(**********************************************************************) +(* session creation and primitive handling *) +(**********************************************************************) + +let create_session () = + let script = + Undo.undoable_view + ~buffer:(GText.buffer ~tag_table:Tags.Script.table ()) + ~wrap_mode:`NONE () in + let proof = + GText.view + ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ()) + ~editable:false ~wrap_mode:`CHAR () in + let message = + GText.view + ~buffer:(GText.buffer ~tag_table:Tags.Message.table ()) + ~editable:false ~wrap_mode:`WORD () in + let basename = + GMisc.label ~text:"*scratch*" () in + let stack = + Stack.create () in + let legacy_av = + new analyzed_view script proof message stack in + let _ = + script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in + let _ = + proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in + let _ = + GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in + let _ = + proof#event#connect#motion_notify ~callback: + (fun e -> + let win = match proof#get_window `WIDGET with + | None -> assert false + | Some w -> w in + let x,y = Gdk.Window.get_pointer_location win in + let b_x,b_y = proof#window_to_buffer_coords ~tag:`WIDGET ~x ~y in + let it = proof#get_iter_at_location ~x:b_x ~y:b_y in + let tags = it#tags in + List.iter + (fun t -> + ignore (GtkText.Tag.event t#as_tag proof#as_widget e it#as_iter)) + tags; + false) in + script#misc#set_name "ScriptWindow"; + script#buffer#place_cursor ~where:(script#buffer#start_iter); + proof#misc#set_can_focus true; + message#misc#set_can_focus true; + script#misc#modify_font !current.text_font; + proof#misc#modify_font !current.text_font; + message#misc#modify_font !current.text_font; + { tab_label=basename; + filename=""; + script=script; + proof_view=proof; + message_view=message; + analyzed_view=legacy_av; + command_stack=stack; + encoding="" + } + +(* XXX - to be used later +let load_session session filename encs = + session.encoding <- List.find (IdeIO.load filename session.script#buffer) encs; + session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); + session.filename <- filename; + session.script#buffer#set_modified false + + +let save_session session filename encs = + session.encoding <- List.find (IdeIO.save session.script#buffer filename) encs; + session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); + session.filename <- filename; + session.script#buffer#set_modified false + + +let init_session session = + session.script#buffer#set_modified false; + session.script#clear_undo; + session.script#buffer#place_cursor session.script#buffer#start_iter + *) + + + + +(*********************************************************************) +(* functions called by the user interface *) +(*********************************************************************) +(* XXX - to be used later +let do_open session filename = + try + load_session session filename ["UTF-8";"ISO-8859-1";"ISO-8859-15"]; + init_session session; + ignore (session_notebook#append_term session) + with _ -> () + + +let do_save session = + try + if session.script#buffer#modified then + save_session session session.filename [session.encoding] + with _ -> () + + +let choose_open = + let last_filename = ref "" in fun session -> + let open_dialog = GWindow.file_chooser_dialog ~action:`OPEN ~title:"Open file" ~modal:true () in + let enc_frame = GBin.frame ~label:"File encoding" ~packing:(open_dialog#vbox#pack ~fill:false) () in + let enc_entry = GEdit.entry ~text:(String.concat " " ["UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in + let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok + ~message:"Invalid encoding, please indicate the encoding to use." () in + let open_response = function + | `OPEN -> begin + match open_dialog#filename with + | Some fn -> begin + try + load_session session fn (Util.split_string_at ' ' enc_entry#text); + session.analyzed_view <- Some (new analyzed_view session); + init_session session; + session_notebook#goto_page (session_notebook#append_term session); + last_filename := fn + with + | Not_found -> open_dialog#misc#hide (); error_dialog#show () + | _ -> + error_dialog#set_markup "Unknown error while loading file, aborting."; + open_dialog#destroy (); error_dialog#destroy () + end + | None -> () + end + | `DELETE_EVENT -> open_dialog#destroy (); error_dialog#destroy () + in + let _ = open_dialog#connect#response open_response in + let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); open_dialog#show ()) in + let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in + let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in + open_dialog#add_select_button_stock `OPEN `OPEN; + open_dialog#add_button_stock `CANCEL `DELETE_EVENT; + open_dialog#add_filter filter_any; + open_dialog#add_filter filter_coq; + ignore(open_dialog#set_filename !last_filename); + open_dialog#show () + + +let choose_save session = + let save_dialog = GWindow.file_chooser_dialog ~action:`SAVE ~title:"Save file" ~modal:true () in + let enc_frame = GBin.frame ~label:"File encoding" ~packing:(save_dialog#vbox#pack ~fill:false) () in + let enc_entry = GEdit.entry ~text:(String.concat " " [session.encoding;"UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in + let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok + ~message:"Invalid encoding, please indicate the encoding to use." () in + let save_response = function + | `SAVE -> begin + match save_dialog#filename with + | Some fn -> begin + try + save_session session fn (Util.split_string_at ' ' enc_entry#text) + with + | Not_found -> save_dialog#misc#hide (); error_dialog#show () + | _ -> + error_dialog#set_markup "Unknown error while saving file, aborting."; + save_dialog#destroy (); error_dialog#destroy () + end + | None -> () + end + | `DELETE_EVENT -> save_dialog#destroy (); error_dialog#destroy () + in + let _ = save_dialog#connect#response save_response in + let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); save_dialog#show ()) in + let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in + let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in + save_dialog#add_select_button_stock `SAVE `SAVE; + save_dialog#add_button_stock `CANCEL `DELETE_EVENT; + save_dialog#add_filter filter_any; + save_dialog#add_filter filter_coq; + ignore(save_dialog#set_filename session.filename); + save_dialog#show () + *) + +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 + + +let main files = (* Statup preferences *) load_pref (); (* Main window *) - let w = GWindow.window + let w = GWindow.window ~wm_class:"CoqIde" ~wm_name:"CoqIde" - ~allow_grow:true ~allow_shrink:true - ~width:!current.window_width ~height:!current.window_height + ~allow_grow:true ~allow_shrink:true + ~width:!current.window_width ~height:!current.window_height ~title:"CoqIde" () in (try @@ -1852,15 +1694,15 @@ let main files = let menubar = GMenu.menu_bar ~packing:vbox#pack () in (* Toolbar *) - let toolbar = GButton.toolbar - ~orientation:`HORIZONTAL + let toolbar = GButton.toolbar + ~orientation:`HORIZONTAL ~style:`ICONS - ~tooltips:true + ~tooltips:true ~packing:(* handle#add *) (vbox#pack ~expand:false ~fill:false) () in - show_toolbar := + show_toolbar := (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ()); let factory = new GMenu.factory ~accel_path:"/" menubar in @@ -1873,17 +1715,20 @@ let main files = (* File/Load Menu *) let load_file handler f = - let f = absolute_filename f in + let f = absolute_filename f in try prerr_endline "Loading file starts"; - Vector.find_or_fail - (function - | {analyzed_view=Some av} -> - (match av#filename with - | None -> false - | Some fn -> same_file f fn) - | _ -> false) - !input_views; + if not (Util.list_fold_left_i + (fun i found x -> if found then found else + let {analyzed_view=av} = x in + (match av#filename with + | None -> false + | Some fn -> + if same_file f fn + then (session_notebook#goto_page i; true) + else false)) + 0 false session_notebook#pages) + then begin prerr_endline "Loading: must open"; let b = Buffer.create 1024 in prerr_endline "Loading: get raw content"; @@ -1891,290 +1736,231 @@ let main files = prerr_endline "Loading: convert content"; let s = do_convert (Buffer.contents b) in prerr_endline "Loading: create view"; - let view = create_input_tab (Glib.Convert.filename_to_utf8 - (Filename.basename f)) - in - prerr_endline "Loading: change font"; - view#misc#modify_font !current.text_font; + let session = create_session () in + session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename f)); prerr_endline "Loading: adding view"; - let index = add_input_view {view = view; - analyzed_view = None; - } - in - let av = (new analyzed_view index) in - prerr_endline "Loading: register view"; - (get_input_view index).analyzed_view <- Some av; + let index = session_notebook#append_term session in + let av = session.analyzed_view in prerr_endline "Loading: set filename"; av#set_filename (Some f); prerr_endline "Loading: stats"; av#update_stats; - let input_buffer = view#buffer in + let input_buffer = session.script#buffer in prerr_endline "Loading: fill buffer"; input_buffer#set_text s; input_buffer#place_cursor input_buffer#start_iter; prerr_endline ("Loading: switch to view "^ string_of_int index); - set_current_view index; - set_tab_image index ~icon:`YES; + session_notebook#goto_page index; prerr_endline "Loading: highlight"; - Highlight.highlight_all input_buffer; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; - av#view#clear_undo; + session.script#clear_undo; prerr_endline "Loading: success" - with - | Vector.Found i -> set_current_view i + end + with | 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" + let load f = load_file flash_info f in + let load_m = file_factory#add_item "_New" ~key:GdkKeysyms._N in - let load_f () = - match select_file_for_save ~title:"Create file" () with + 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" + let load_m = file_factory#add_item "_Open" ~key:GdkKeysyms._O in - let load_f () = - match select_file_for_open ~title:"Load file" () with + let load_f () = + match select_file_for_open ~title:"Load file" () with | None -> () | Some f -> load f in ignore (load_m#connect#activate (load_f)); (* File/Save Menu *) - let save_m = file_factory#add_item "_Save" + let save_m = file_factory#add_item "_Save" ~key:GdkKeysyms._S in - - - let save_f () = - let current = get_current_view () in + let save_f () = + let current = session_notebook#current_term in try - (match (Option.get current.analyzed_view)#filename with + (match current.analyzed_view#filename with | None -> begin match select_file_for_save ~title:"Save file" () with | None -> () - | Some f -> - if (Option.get current.analyzed_view)#save_as f then begin - set_current_tab_label (Filename.basename f); - !flash_info ("File " ^ f ^ " saved") + | Some f -> + if current.analyzed_view#save_as f then begin + current.tab_label#set_text (Filename.basename f); + flash_info ("File " ^ f ^ " saved") end else warning ("Save Failed (check if " ^ f ^ " is writable)") end - | Some f -> - if (Option.get current.analyzed_view)#save f then - !flash_info ("File " ^ f ^ " saved") + | Some f -> + if current.analyzed_view#save f then + flash_info ("File " ^ f ^ " saved") else warning ("Save Failed (check if " ^ f ^ " is writable)") - + ) - with + with | e -> warning "Save: unexpected error" - in + in ignore (save_m#connect#activate save_f); (* File/Save As Menu *) - let saveas_m = file_factory#add_item "S_ave as" + let saveas_m = file_factory#add_item "S_ave as" in - let saveas_f () = - let current = get_current_view () in - try (match (Option.get current.analyzed_view)#filename with - | None -> + let saveas_f () = + let current = session_notebook#current_term in + try (match current.analyzed_view#filename with + | None -> begin match select_file_for_save ~title:"Save file as" () with | None -> () - | Some f -> - if (Option.get current.analyzed_view)#save_as f then begin - set_current_tab_label (Filename.basename f); - !flash_info "Saved" + | Some f -> + if current.analyzed_view#save_as f then begin + current.tab_label#set_text (Filename.basename f); + flash_info "Saved" end - else !flash_info "Save Failed" + else flash_info "Save Failed" end - | Some f -> - begin match select_file_for_save - ~dir:(ref (Filename.dirname f)) + | Some f -> + begin match select_file_for_save + ~dir:(ref (Filename.dirname f)) ~filename:(Filename.basename f) ~title:"Save file as" () with | None -> () - | Some f -> - 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" + | Some f -> + if current.analyzed_view#save_as f then begin + current.tab_label#set_text (Filename.basename f); + flash_info "Saved" + end else flash_info "Save Failed" end); - with e -> !flash_info "Save Failed" - in + with e -> flash_info "Save Failed" + in ignore (saveas_m#connect#activate saveas_f); - + (* XXX *) (* File/Save All Menu *) let saveall_m = file_factory#add_item "Sa_ve all" in - let saveall_f () = - Vector.iter - (function - | {view = view ; analyzed_view = Some av} -> - begin match av#filename with + let saveall_f () = + List.iter + (function + | {script = view ; analyzed_view = av} -> + begin match av#filename with | None -> () | Some f -> ignore (av#save f) end - | _ -> () - ) input_views + ) session_notebook#pages in - let has_something_to_save () = - Vector.exists - (function - | {view=view} -> view#buffer#modified + (* XXX *) + let has_something_to_save () = + List.exists + (function + | {script=view} -> view#buffer#modified ) - input_views + session_notebook#pages in ignore (saveall_m#connect#activate saveall_f); - + (* XXX *) (* File/Revert Menu *) let revert_m = file_factory#add_item "_Revert all buffers" in - let revert_f () = - Vector.iter - (function - {view = view ; analyzed_view = Some av} -> - (try - match av#filename,av#stats with - | Some f,Some stats -> + let revert_f () = + List.iter + (function + {analyzed_view = av} -> + (try + match av#filename,av#stats with + | Some f,Some stats -> let new_stats = Unix.stat f in - if new_stats.Unix.st_mtime > stats.Unix.st_mtime + if new_stats.Unix.st_mtime > stats.Unix.st_mtime then av#revert | Some _, None -> av#revert | _ -> () with _ -> av#revert) - | _ -> () - ) input_views + ) session_notebook#pages in ignore (revert_m#connect#activate revert_f); - + (* File/Close Menu *) let close_m = file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in - let close_f () = - 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" + let close_f () = + let v = !active_view in + let act = session_notebook#current_page in + if v = act then flash_info "Cannot close an active view" else remove_current_view_page () in ignore (close_m#connect#activate close_f); - + (* File/Print Menu *) - let print_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in - match av#filename with - | None -> - !flash_info "Cannot print: this buffer has no name" - | Some f -> - let cmd = - "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ - !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^ - " | " ^ !current.cmd_print - in - 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..." ~key:GdkKeysyms._P - ~callback:print_f in + ~callback:(fun () -> do_print session_notebook#current_term) in (* File/Export to Menu *) let export_f kind () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in match av#filename with - | None -> - !flash_info "Cannot print: this buffer has no name" + | None -> + flash_info "Cannot print: this buffer has no name" | Some f -> let basef = Filename.basename f in - let output = + let output = let basef_we = try Filename.chop_extension basef with _ -> basef in match kind with | "latex" -> basef_we ^ ".tex" | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind | _ -> assert false in - let cmd = + let cmd = "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 - !flash_info (cmd ^ - if s = Unix.WEXITED 0 - then " succeeded" + flash_info (cmd ^ + if s = Unix.WEXITED 0 + then " succeeded" else " failed") in let file_export_m = file_factory#add_submenu "E_xport to" in let file_export_factory = new GMenu.factory ~accel_path:"/Export/" file_export_m ~accel_group in - let _ = - file_export_factory#add_item "_Html" ~callback:(export_f "html") + let _ = + file_export_factory#add_item "_Html" ~callback:(export_f "html") in - let _ = + let _ = file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex") in - let _ = - file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") + let _ = + file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") in - let _ = - file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf") + let _ = + file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf") in - let _ = - file_export_factory#add_item "_Ps" ~callback:(export_f "ps") + let _ = + file_export_factory#add_item "_Ps" ~callback:(export_f "ps") in (* File/Rehighlight Menu *) let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in - ignore (rehighlight_m#connect#activate - (fun () -> - Highlight.highlight_all - (get_current_view()).view#buffer; - (Option.get (get_current_view()).analyzed_view)#recenter_insert)); + ignore (rehighlight_m#connect#activate + (fun () -> + force_retag + session_notebook#current_term.script#buffer; + session_notebook#current_term.analyzed_view#recenter_insert)); (* File/Quit Menu *) let quit_f () = save_pref(); - if has_something_to_save () then + if has_something_to_save () then match (GToolbox.question_box ~title:"Quit" ~buttons:["Save Named Buffers and Quit"; "Quit without Saving"; - "Don't Quit"] + "Don't Quit"] ~default:0 ~icon: (let img = GMisc.image () in @@ -2188,7 +1974,7 @@ let main files = | _ -> () else exit 0 in - let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q + let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q ~callback:quit_f in ignore (w#event#connect#delete (fun _ -> quit_f (); true)); @@ -2198,50 +1984,60 @@ let main files = let edit_f = new GMenu.factory ~accel_path:"/Edit/" edit_menu ~accel_group in ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback: (do_if_not_computing "undo" - (fun () -> - 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" + (fun () -> + ignore (session_notebook#current_term.analyzed_view# + without_auto_complete + (fun () -> session_notebook#current_term.script#undo) ())))); + ignore(edit_f#add_item "_Clear Undo Stack" (* ~key:GdkKeysyms._exclam *) ~callback: - (fun () -> - ignore (get_current_view()).view#clear_undo)); + (fun () -> + ignore session_notebook#current_term.script#clear_undo)); ignore(edit_f#add_separator ()); + let get_active_view_for_cp () = + let has_sel (i0,i1) = i0#compare i1 <> 0 in + let current = session_notebook#current_term in + if has_sel current.script#buffer#selection_bounds + then current.script#as_view + else if has_sel current.proof_view#buffer#selection_bounds + then current.proof_view#as_view + else current.message_view#as_view + in ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback: (fun () -> GtkSignal.emit_unit - (get_current_view()).view#as_view - GtkText.View.S.cut_clipboard)); + (get_active_view_for_cp ()) + GtkText.View.S.cut_clipboard + )); ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback: (fun () -> GtkSignal.emit_unit - (get_current_view()).view#as_view + (get_active_view_for_cp ()) GtkText.View.S.copy_clipboard)); ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback: - (fun () -> + (fun () -> try GtkSignal.emit_unit - (get_current_view()).view#as_view + session_notebook#current_term.script#as_view GtkText.View.S.paste_clipboard with _ -> prerr_endline "EMIT PASTE FAILED")); ignore (edit_f#add_separator ()); (* - let toggle_auto_complete_i = - edit_f#add_check_item "_Auto Completion" + let toggle_auto_complete_i = + edit_f#add_check_item "_Auto Completion" ~active:!current.auto_complete ~callback: in *) (* - auto_complete := - (fun b -> match (get_current_view()).analyzed_view with + auto_complete := + (fun b -> match session_notebook#current_term.analyzed_view with | Some av -> av#set_auto_complete b | None -> ()); *) let last_found = ref None in let search_backward = ref false in - let find_w = GWindow.window + let find_w = GWindow.window (* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *) (* ~allow_grow:true ~allow_shrink:true *) (* ~width:!current.window_width ~height:!current.window_height *) @@ -2252,38 +2048,38 @@ let main files = ~columns:3 ~rows:5 ~col_spacings:10 ~row_spacings:10 ~border_width:10 ~homogeneous:false ~packing:find_w#add () in - - let _ = + + let _ = GMisc.label ~text:"Find:" ~xalign:1.0 - ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () + ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () in let find_entry = GEdit.entry ~editable: true ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X) () in - let _ = + let _ = GMisc.label ~text:"Replace with:" ~xalign:1.0 - ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () + ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () in let replace_entry = GEdit.entry ~editable: true ~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 *) (* - let find_backwards_check = + let find_backwards_check = GButton.check_button ~label:"search backwards" ~active:false @@ -2322,25 +2118,25 @@ let main files = () in let last_find () = - let v = (get_current_view()).view in + let v = session_notebook#current_term.script in let b = v#buffer in let start,stop = - match !last_found with + match !last_found with | None -> let i = b#get_iter_at_mark `INSERT in (i,i) | Some(start,stop) -> let start = b#get_iter_at_mark start and stop = b#get_iter_at_mark stop in - b#remove_tag_by_name ~start ~stop "found"; + b#remove_tag Tags.Script.found ~start ~stop; last_found:=None; start,stop in (v,b,start,stop) in let do_replace () = - let v = (get_current_view()).view in + let v = session_notebook#current_term.script in let b = v#buffer in - match !last_found with + match !last_found with | None -> () | Some(start,stop) -> let start = b#get_iter_at_mark start @@ -2358,7 +2154,7 @@ let main files = with | None -> () | Some(start,stop) -> - b#apply_tag_by_name "found" ~start ~stop; + b#apply_tag Tags.Script.found ~start ~stop; let start = `MARK (b#create_mark start) and stop = `MARK (b#create_mark stop) in @@ -2368,7 +2164,7 @@ let main files = in let do_find () = let (v,b,starti,_) = last_find () in - find_from v b starti find_entry#text + find_from v b starti find_entry#text in let do_replace_find () = do_replace(); @@ -2380,8 +2176,8 @@ let main files = find_w#misc#hide(); v#coerce#misc#grab_focus() in - to_do_on_page_switch := - (fun i -> if find_w#misc#visible then close_find()):: + to_do_on_page_switch := + (fun i -> if find_w#misc#visible then close_find()):: !to_do_on_page_switch; let find_again_forward () = search_backward := false; @@ -2403,12 +2199,12 @@ let main files = find_w#misc#hide(); v#coerce#misc#grab_focus(); true - end + end else if k = GdkKeysyms._Return then begin close_find(); true - end + end else if List.mem `CONTROL s && k = GdkKeysyms._f then begin find_again_forward (); @@ -2421,7 +2217,7 @@ let main files = end else false (* to let default callback execute *) in - let find_f ~backward () = + let find_f ~backward () = search_backward := backward; find_w#show (); find_w#present (); @@ -2455,30 +2251,30 @@ let main files = let complete_i = edit_f#add_item "_Complete" ~key:GdkKeysyms._comma ~callback: - (do_if_not_computing - (fun b -> - let v = Option.get (get_current_view ()).analyzed_view - - in v#complete_at_offset + (do_if_not_computing + (fun b -> + let v = session_notebook#current_term.analyzed_view + + in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset) )) in complete_i#misc#set_state `INSENSITIVE; *) - + ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: - (fun () -> + (fun () -> ignore ( - let av = Option.get ((get_current_view()).analyzed_view) in + let av = session_notebook#current_term.analyzed_view in av#complete_at_offset (av#get_insert)#offset ))); ignore(edit_f#add_separator ()); (* external editor *) - let _ = + let _ = edit_f#add_item "External editor" ~callback: - (fun () -> - let av = Option.get ((get_current_view()).analyzed_view) in + (fun () -> + let av = session_notebook#current_term.analyzed_view in match av#filename with | None -> warning "Call to external editor available only on named files" | Some f -> @@ -2491,34 +2287,33 @@ let main files = (* Preferences *) let reset_revert_timer () = disconnect_revert_timer (); - if !current.global_auto_revert then + if !current.global_auto_revert then revert_timer := Some - (GMain.Timeout.add ~ms:!current.global_auto_revert_delay + (GMain.Timeout.add ~ms:!current.global_auto_revert_delay ~callback: - (fun () -> + (fun () -> do_if_not_computing "revert" (sync revert_f) (); true)) in reset_revert_timer (); (* to enable statup preferences timer *) - - let auto_save_f () = - Vector.iter - (function - {view = view ; analyzed_view = Some av} -> - (try + (* XXX *) + let auto_save_f () = + List.iter + (function + {script = view ; analyzed_view = av} -> + (try av#auto_save with _ -> ()) - | _ -> () - ) - input_views + ) + session_notebook#pages in let reset_auto_save_timer () = disconnect_auto_save_timer (); - if !current.auto_save then + if !current.auto_save then auto_save_timer := Some - (GMain.Timeout.add ~ms:!current.auto_save_delay + (GMain.Timeout.add ~ms:!current.auto_save_delay ~callback: - (fun () -> + (fun () -> do_if_not_computing "autosave" (sync auto_save_f) (); true)) in reset_auto_save_timer (); (* to enable statup preferences timer *) @@ -2536,34 +2331,40 @@ let main files = *) (* Navigation Menu *) let navigation_menu = factory#add_submenu "_Navigation" in - let navigation_factory = - new GMenu.factory navigation_menu + let navigation_factory = + new GMenu.factory navigation_menu ~accel_path:"/Navigation/" - ~accel_group - ~accel_modi:!current.modifier_for_navigation + ~accel_group + ~accel_modi:!current.modifier_for_navigation in - let do_or_activate f () = - let current = get_current_view () in - let analyzed_view = Option.get current.analyzed_view in - if analyzed_view#is_active then + let _do_or_activate f () = + let current = session_notebook#current_term in + let analyzed_view = current.analyzed_view in + if analyzed_view#is_active then begin + prerr_endline ("view "^current.tab_label#text^"already active"); ignore (f analyzed_view) - else + end else begin - !flash_info "New proof started"; - activate_input (notebook ())#current_page; + flash_info "New proof started"; + prerr_endline ("activating view "^current.tab_label#text); + activate_input session_notebook#current_page; ignore (f analyzed_view) end in - let do_or_activate f = + let do_or_activate f = do_if_not_computing "do_or_activate" - (do_or_activate - (fun av -> f av ; !pop_info();!push_info (Coq.current_status()))) + (_do_or_activate + (fun av -> f av; + pop_info (); + push_info (Coq.current_status()) + ) + ) in - let add_to_menu_toolbar text ~tooltip ?key ~callback icon = + let add_to_menu_toolbar text ~tooltip ?key ~callback icon = begin - match key with None -> () + match key with None -> () | Some key -> ignore (navigation_factory#add_item text ~key ~callback) end; ignore (toolbar#insert_button @@ -2573,107 +2374,106 @@ let main files = ~callback ()) in - add_to_menu_toolbar - "_Save" - ~tooltip:"Save current buffer" + add_to_menu_toolbar + "_Save" + ~tooltip:"Save current buffer" ~callback:save_f `SAVE; - add_to_menu_toolbar - "_Close" - ~tooltip:"Close current buffer" + add_to_menu_toolbar + "_Close" + ~tooltip:"Close current buffer" ~callback:close_f `CLOSE; - add_to_menu_toolbar - "_Forward" - ~tooltip:"Forward one command" - ~key:GdkKeysyms._Down - ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true)) + add_to_menu_toolbar + "_Forward" + ~tooltip:"Forward one command" + ~key:GdkKeysyms._Down + ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true )) + `GO_DOWN; add_to_menu_toolbar "_Backward" - ~tooltip:"Backward one command" + ~tooltip:"Backward one command" ~key:GdkKeysyms._Up ~callback:(do_or_activate (fun a -> a#undo_last_step)) `GO_UP; - add_to_menu_toolbar - "_Go to" - ~tooltip:"Go to cursor" + add_to_menu_toolbar + "_Go to" + ~tooltip:"Go to cursor" ~key:GdkKeysyms._Right ~callback:(do_or_activate (fun a-> a#go_to_insert)) `JUMP_TO; - add_to_menu_toolbar - "_Start" - ~tooltip:"Go to start" + add_to_menu_toolbar + "_Start" + ~tooltip:"Go to start" ~key:GdkKeysyms._Home ~callback:(do_or_activate (fun a -> a#reset_initial)) `GOTO_TOP; - add_to_menu_toolbar - "_End" - ~tooltip:"Go to end" + add_to_menu_toolbar + "_End" + ~tooltip:"Go to end" ~key:GdkKeysyms._End ~callback:(do_or_activate (fun a -> a#process_until_end_or_error)) `GOTO_BOTTOM; add_to_menu_toolbar "_Interrupt" - ~tooltip:"Interrupt computations" - ~key:GdkKeysyms._Break + ~tooltip:"Interrupt computations" + ~key:GdkKeysyms._Break ~callback:break `STOP; + add_to_menu_toolbar "_Hide" + ~tooltip:"Hide proof" + ~key:GdkKeysyms._h + ~callback:(fun x -> + let sess = session_notebook#current_term in + toggle_proof_visibility sess.script#buffer + sess.analyzed_view#get_insert) + `MISSING_IMAGE; (* Tactics Menu *) let tactics_menu = factory#add_submenu "_Try Tactics" in - let tactics_factory = - new GMenu.factory tactics_menu + let tactics_factory = + new GMenu.factory tactics_menu ~accel_path:"/Tactics/" - ~accel_group + ~accel_group ~accel_modi:!current.modifier_for_tactics in - let do_if_active_raw f () = - let current = get_current_view () in - let analyzed_view = Option.get current.analyzed_view in + let do_if_active_raw f () = + let current = session_notebook#current_term in + let analyzed_view = current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) in let do_if_active f = do_if_not_computing "do_if_active" (do_if_active_raw f) in - (* - let blaster_i = - tactics_factory#add_item "_Blaster" - ~key:GdkKeysyms._b - ~callback: (do_if_active_raw (fun a -> a#blaster ())) - (* Custom locking mechanism! *) - in - blaster_i#misc#set_state `INSENSITIVE; - *) - - ignore (tactics_factory#add_item "_auto" + ignore (tactics_factory#add_item "_auto" ~key:GdkKeysyms._a ~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n")) ); ignore (tactics_factory#add_item "_auto with *" ~key:GdkKeysyms._asterisk - ~callback:(do_if_active (fun a -> a#insert_command + ~callback:(do_if_active (fun a -> a#insert_command "progress auto with *.\n" "auto with *.\n"))); ignore (tactics_factory#add_item "_eauto" ~key:GdkKeysyms._e - ~callback:(do_if_active (fun a -> a#insert_command + ~callback:(do_if_active (fun a -> a#insert_command "progress eauto.\n" "eauto.\n")) ); ignore (tactics_factory#add_item "_eauto with *" ~key:GdkKeysyms._ampersand - ~callback:(do_if_active (fun a -> a#insert_command - "progress eauto with *.\n" + ~callback:(do_if_active (fun a -> a#insert_command + "progress eauto with *.\n" "eauto with *.\n")) ); ignore (tactics_factory#add_item "_intuition" ~key:GdkKeysyms._i - ~callback:(do_if_active (fun a -> a#insert_command - "progress intuition.\n" + ~callback:(do_if_active (fun a -> a#insert_command + "progress intuition.\n" "intuition.\n")) ); ignore (tactics_factory#add_item "_omega" ~key:GdkKeysyms._o - ~callback:(do_if_active (fun a -> a#insert_command + ~callback:(do_if_active (fun a -> a#insert_command "omega.\n" "omega.\n")) ); ignore (tactics_factory#add_item "_simpl" @@ -2703,15 +2503,15 @@ let main files = ignore (tactics_factory#add_item "" ~key:GdkKeysyms._dollar - ~callback:(do_if_active (fun a -> a#tactic_wizard + ~callback:(do_if_active (fun a -> a#tactic_wizard !current.automatic_tactics )) ); - + ignore (tactics_factory#add_separator ()); - let add_simple_template (factory: GMenu.menu GMenu.factory) + let add_simple_template (factory: GMenu.menu GMenu.factory) (menu_text, text) = - let text = + let text = let l = String.length text - 1 in if String.get text l = '.' then text ^"\n" @@ -2719,42 +2519,42 @@ let main files = in ignore (factory#add_item menu_text ~callback: - (fun () -> let {view = view } = get_current_view () in + (fun () -> let {script = view } = session_notebook#current_term in ignore (view#buffer#insert_interactive text))) in - List.iter - (fun l -> - match l with + List.iter + (fun l -> + match l with | [] -> () - | [s] -> add_simple_template tactics_factory ("_"^s, s) - | s::_ -> + | [s] -> add_simple_template tactics_factory ("_"^s, s) + | s::_ -> let a = "_@..." in a.[1] <- s.[0]; - let f = tactics_factory#add_submenu a in + let f = tactics_factory#add_submenu a in let ff = new GMenu.factory f ~accel_group in - List.iter - (fun x -> + List.iter + (fun x -> add_simple_template - ff + ff ((String.sub x 0 1)^ "_"^ (String.sub x 1 (String.length x - 1)), x)) l - ) + ) Coq_commands.tactics; - + (* Templates Menu *) let templates_menu = factory#add_submenu "Te_mplates" in - let templates_factory = new GMenu.factory templates_menu + let templates_factory = new GMenu.factory templates_menu ~accel_path:"/Templates/" - ~accel_group + ~accel_group ~accel_modi:!current.modifier_for_templates in let add_complex_template (menu_text, text, offset, len, key) = (* Templates/Lemma *) let callback () = - let {view = view } = get_current_view () in + let {script = view } = session_notebook#current_term in if view#buffer#insert_interactive text then begin let iter = view#buffer#get_iter_at_mark `INSERT in ignore (iter#nocopy#backward_chars offset); @@ -2764,19 +2564,19 @@ let main files = end in ignore (templates_factory#add_item menu_text ~callback ?key) in - add_complex_template - ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", + add_complex_template + ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", 19, 9, Some GdkKeysyms._L); - add_complex_template - ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", + add_complex_template + ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", 19, 11, Some GdkKeysyms._T); - add_complex_template + add_complex_template ("_Definition __", "Definition ident := .\n", 6, 5, Some GdkKeysyms._D); - add_complex_template + add_complex_template ("_Inductive __", "Inductive ident : :=\n | : .\n", 14, 5, Some GdkKeysyms._I); - add_complex_template + add_complex_template ("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 29, 5, Some GdkKeysyms._F); add_complex_template("_Scheme __", @@ -2784,14 +2584,14 @@ let main files = with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Template for match *) - let callback () = + let callback () = let w = get_current_word () in - try + try let cases = Coq.make_cases w in let print c = function | [x] -> Format.fprintf c " | %s => _@\n" x - | x::l -> Format.fprintf c " | (%s%a) => _@\n" x + | x::l -> Format.fprintf c " | (%s%a) => _@\n" x (print_list (fun c s -> Format.fprintf c " %s" s)) l | [] -> assert false in @@ -2801,28 +2601,28 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (print_list print) cases; let s = Buffer.contents b in prerr_endline s; - let {view = view } = get_current_view () in + let {script = view } = session_notebook#current_term in ignore (view#buffer#delete_selection ()); - let m = view#buffer#create_mark + let m = view#buffer#create_mark (view#buffer#get_iter `INSERT) in - if view#buffer#insert_interactive s then + if view#buffer#insert_interactive s then let i = view#buffer#get_iter (`MARK m) in let _ = i#nocopy#forward_chars 9 in view#buffer#place_cursor i; view#buffer#move_mark ~where:(i#backward_chars 3) - `SEL_BOUND - with Not_found -> !flash_info "Not an inductive type" + `SEL_BOUND + with Not_found -> flash_info "Not an inductive type" in ignore (templates_factory#add_item "match ..." ~key:GdkKeysyms._C ~callback ); - + (* - let add_simple_template (factory: GMenu.menu GMenu.factory) + let add_simple_template (factory: GMenu.menu GMenu.factory) (menu_text, text) = - let text = + let text = let l = String.length text - 1 in if String.get text l = '.' then text ^"\n" @@ -2830,7 +2630,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in ignore (factory#add_item menu_text ~callback: - (fun () -> let {view = view } = get_current_view () in + (fun () -> let {view = view } = session_notebook#current_term in ignore (view#buffer#insert_interactive text))) in *) @@ -2849,92 +2649,100 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ]; ignore (templates_factory#add_separator ()); *) - List.iter - (fun l -> - match l with + List.iter + (fun l -> + match l with | [] -> () - | [s] -> add_simple_template templates_factory ("_"^s, s) - | s::_ -> + | [s] -> add_simple_template templates_factory ("_"^s, s) + | s::_ -> let a = "_@..." in a.[1] <- s.[0]; - let f = templates_factory#add_submenu a in + let f = templates_factory#add_submenu a in let ff = new GMenu.factory f ~accel_group in - List.iter - (fun x -> - add_simple_template - ff + List.iter + (fun x -> + add_simple_template + ff ((String.sub x 0 1)^ "_"^ (String.sub x 1 (String.length x - 1)), x)) l - ) + ) Coq_commands.commands; - + (* Queries Menu *) let queries_menu = factory#add_submenu "_Queries" in let queries_factory = new GMenu.factory queries_menu ~accel_group ~accel_path:"/Queries" ~accel_modi:[] in - + (* Command/Show commands *) - let _ = + let _ = queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"SearchAbout" - ~term + ~term ()) in - let _ = + let _ = queries_factory#add_item "_Check " ~key:GdkKeysyms._F3 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Check" - ~term + ~term ()) in - let _ = + let _ = queries_factory#add_item "_Print " ~key:GdkKeysyms._F4 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Print" - ~term + ~term + ()) + in + let _ = + queries_factory#add_item "_About " ~key:GdkKeysyms._F5 + ~callback:(fun () -> let term = get_current_word () in + (Command_windows.command_window ())#new_command + ~command:"About" + ~term ()) in - let _ = - queries_factory#add_item "_Locate" + let _ = + queries_factory#add_item "_Locate" ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Locate" - ~term + ~term ()) in - let _ = - queries_factory#add_item "_Whelp Locate" + let _ = + queries_factory#add_item "_Whelp Locate" ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Whelp Locate" - ~term + ~term ()) in (* Display menu *) - + let display_menu = factory#add_submenu "_Display" in let view_factory = new GMenu.factory display_menu ~accel_path:"/Display/" - ~accel_group + ~accel_group ~accel_modi:!current.modifier_for_display in - let _ = ignore (view_factory#add_check_item - "Display _implicit arguments" + 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 + 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 @@ -2944,104 +2752,77 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~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 + 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 + 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 + ~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 + 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 + 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 + 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 + ~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:"/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:"/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 + let externals_factory = new GMenu.factory externals_menu ~accel_path:"/Compile/" - ~accel_group + ~accel_group ~accel_modi:[] in - + (* Command/Compile Menu *) let compile_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in save_f (); match av#filename with - | None -> - !flash_info "Active buffer has no name" + | None -> + flash_info "Active buffer has no name" | Some f -> - let cmd = !current.cmd_coqc ^ " -I " + let cmd = !current.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f)) ^ " " ^ (Filename.quote f) in let s,res = run_command av#insert_message cmd in if s = Unix.WEXITED 0 then - !flash_info (f ^ " successfully compiled") + flash_info (f ^ " successfully compiled") else begin - !flash_info (f ^ " failed to compile"); - activate_input (notebook ())#current_page; + flash_info (f ^ " failed to compile"); + activate_input session_notebook#current_page; av#process_until_end_or_error; av#insert_message "Compilation output:\n"; av#insert_message res end in - let _ = - externals_factory#add_item "_Compile Buffer" ~callback:compile_f + let _ = + externals_factory#add_item "_Compile Buffer" ~callback:compile_f in (* Command/Make Menu *) let make_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in match av#filename with - | None -> - !flash_info "Cannot make: this buffer has no name" + | None -> + flash_info "Cannot make: this buffer has no name" | Some f -> - let cmd = + let cmd = "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in (* @@ -3051,22 +2832,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); 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") + flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in - let _ = externals_factory#add_item "_Make" + let _ = externals_factory#add_item "_Make" ~key:GdkKeysyms._F6 - ~callback:make_f + ~callback:make_f in - + (* Compile/Next Error *) - let next_error () = + let next_error () = try let file,line,start,stop,error_msg = search_next_error () in - load file; - let v = get_current_view () in - let av = Option.get v.analyzed_view in - let input_buffer = v.view#buffer in + load file; + let v = session_notebook#current_term in + let av = v.analyzed_view in + let input_buffer = v.script#buffer in (* let init = input_buffer#start_iter in let i = init#forward_lines (line-1) in @@ -3082,215 +2863,143 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); *) let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in - input_buffer#apply_tag_by_name "error" + input_buffer#apply_tag Tags.Script.error ~start:starti ~stop:stopi; input_buffer#place_cursor starti; av#set_message error_msg; - v.view#misc#grab_focus () + v.script#misc#grab_focus () with Not_found -> last_make_index := 0; - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in av#set_message "No more errors.\n" in - let _ = - externals_factory#add_item "_Next error" + let _ = + externals_factory#add_item "_Next error" ~key:GdkKeysyms._F7 ~callback:next_error in - + (* Command/CoqMakefile Menu*) let coq_makefile_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in match av#filename with - | None -> - !flash_info "Cannot make makefile: this buffer has no name" + | None -> + flash_info "Cannot make makefile: this buffer has no name" | Some f -> - let cmd = + let cmd = "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in let s,res = run_command av#insert_message cmd in - !flash_info + flash_info (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in - let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f + let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f in (* Windows Menu *) let configuration_menu = factory#add_submenu "_Windows" in - let configuration_factory = new GMenu.factory configuration_menu + let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"/Windows" ~accel_modi:[] ~accel_group in let _ = - configuration_factory#add_item + configuration_factory#add_item "Show/Hide _Query Pane" ~key:GdkKeysyms._Escape - ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then + ~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_check_item - "Show/Hide _Toolbar" - ~callback:(fun _ -> - !current.show_toolbar <- not !current.show_toolbar; - !show_toolbar !current.show_toolbar) - in - let _ = configuration_factory#add_item - "Detach _Script Window" - ~callback: - (do_if_not_computing "detach script window" (sync - (fun () -> - let nb = notebook () in - if nb#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) - ~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)); - nw#add_accel_group accel_group; - nb#misc#reparent nw#coerce - 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 - ))) + let _ = + configuration_factory#add_check_item + "Show/Hide _Toolbar" + ~callback:(fun _ -> + !current.show_toolbar <- not !current.show_toolbar; + !show_toolbar !current.show_toolbar) in -*) - let _ = - configuration_factory#add_item + let _ = + configuration_factory#add_item "Detach _View" ~callback: (do_if_not_computing "detach view" - (fun () -> - match get_current_view () with - | {view=v;analyzed_view=Some av} -> - let w = GWindow.window ~show:true + (fun () -> + match session_notebook#current_term with + | {script=v;analyzed_view=av} -> + let w = GWindow.window ~show:true ~width:(!current.window_width*2/3) ~height:(!current.window_height*2/3) ~position:`CENTER ~title:(match av#filename with | None -> "*Unnamed*" - | Some f -> f) - () + | Some f -> f) + () in - let sb = GBin.scrolled_window - ~packing:w#add () + let sb = GBin.scrolled_window + ~packing:w#add () in - let nv = GText.view - ~buffer:v#buffer - ~packing:sb#add + let nv = GText.view + ~buffer:v#buffer + ~packing:sb#add () in - nv#misc#modify_font - !current.text_font; - ignore (w#connect#destroy + nv#misc#modify_font + !current.text_font; + ignore (w#connect#destroy ~callback: (fun () -> av#remove_detached_view w)); av#add_detached_view w - | _ -> () - + )) in (* Help Menu *) let help_menu = factory#add_submenu "_Help" in - let help_factory = new GMenu.factory help_menu + let help_factory = new GMenu.factory help_menu ~accel_path:"/Help/" ~accel_modi:[] ~accel_group in - let _ = help_factory#add_item "Browse Coq _Manual" + let _ = help_factory#add_item "Browse Coq _Manual" ~callback: - (fun () -> - let av = Option.get ((get_current_view ()).analyzed_view) in - browse av#insert_message (!current.doc_url)) in - let _ = help_factory#add_item "Browse Coq _Library" + (fun () -> + let av = session_notebook#current_term.analyzed_view in + browse av#insert_message (doc_url ())) in + let _ = help_factory#add_item "Browse Coq _Library" ~callback: - (fun () -> - let av = Option.get ((get_current_view ()).analyzed_view) in + (fun () -> + let av = session_notebook#current_term.analyzed_view in browse av#insert_message !current.library_url) in - let _ = + let _ = help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1 - ~callback:(fun () -> - let av = Option.get ((get_current_view ()).analyzed_view) in + ~callback:(fun () -> + let av = session_notebook#current_term.analyzed_view in av#help_for_keyword ()) in let _ = help_factory#add_separator () in - (* - 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 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 - ()); + queries_pane#pack1 ~shrink:false ~resize:true session_notebook#coerce; 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 sw2 = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:(fr_a#add) () in - let sw3 = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:(fr_b#add) () in + let nb = session_notebook 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 + lower_hbox#pack ~expand:true status#coerce; let search_lbl = GMisc.label ~text:"Search:" ~show:false - ~packing:(lower_hbox#pack ~expand:false) () + ~packing:(lower_hbox#pack ~expand:false) () in let search_history = ref [] in let search_input = GEdit.combo ~popdown_strings:!search_history ~enable_arrow_keys:true ~show:false - ~packing:(lower_hbox#pack ~expand:false) () + ~packing:(lower_hbox#pack ~expand:false) () in search_input#disable_activate (); let ready_to_wrap_search = ref false in @@ -3301,108 +3010,99 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let search_forward = ref true in let matched_word = ref None in - let memo_search () = + let memo_search () = matched_word := Some search_input#entry#text - - (* if not (List.mem search_input#entry#text !search_history) then - (search_history := - search_input#entry#text::!search_history; - search_input#set_popdown_strings !search_history); - start_of_search := None; - ready_to_wrap_search := false - *) - in - let end_search () = + let end_search () = prerr_endline "End Search"; memo_search (); - let v = (get_current_view ()).view in + let v = session_notebook#current_term.script in v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT); v#coerce#misc#grab_focus (); search_input#entry#set_text ""; search_lbl#misc#hide (); search_input#misc#hide () in - let end_search_focus_out () = + let end_search_focus_out () = prerr_endline "End Search(focus out)"; memo_search (); - let v = (get_current_view ()).view in + let v = session_notebook#current_term.script in v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT); search_input#entry#set_text ""; search_lbl#misc#hide (); search_input#misc#hide () in ignore (search_input#entry#connect#activate ~callback:end_search); - ignore (search_input#entry#event#connect#key_press + ignore (search_input#entry#event#connect#key_press ~callback:(fun k -> let kv = GdkEvent.Key.keyval k in - if + if kv = GdkKeysyms._Right - || kv = GdkKeysyms._Up + || kv = GdkKeysyms._Up || kv = GdkKeysyms._Left - || (kv = GdkKeysyms._g + || (kv = GdkKeysyms._g && (List.mem `CONTROL (GdkEvent.Key.state k))) - then end_search (); + then end_search (); false)); ignore (search_input#entry#event#connect#focus_out ~callback:(fun _ -> end_search_focus_out (); false)); - to_do_on_page_switch := - (fun i -> + to_do_on_page_switch := + (fun i -> start_of_search := None; ready_to_wrap_search:=false)::!to_do_on_page_switch; (* TODO : make it work !!! *) - let rec search_f () = + let rec search_f () = search_lbl#misc#show (); search_input#misc#show (); prerr_endline "search_f called"; if !start_of_search = None then begin (* A full new search is starting *) - start_of_search := - Some ((get_current_view ()).view#buffer#create_mark - ((get_current_view ()).view#buffer#get_iter_at_mark `INSERT)); + start_of_search := + Some (session_notebook#current_term.script#buffer#create_mark + (session_notebook#current_term.script#buffer#get_iter_at_mark `INSERT)); start_of_found := !start_of_search; end_of_found := !start_of_search; matched_word := Some ""; end; - let txt = search_input#entry#text in - let v = (get_current_view ()).view in - let iit = v#buffer#get_iter_at_mark `SEL_BOUND + let txt = search_input#entry#text in + let v = session_notebook#current_term.script in + let iit = v#buffer#get_iter_at_mark `SEL_BOUND and insert_iter = v#buffer#get_iter_at_mark `INSERT in prerr_endline ("SELBOUND="^(string_of_int iit#offset)); prerr_endline ("INSERT="^(string_of_int insert_iter#offset)); - + (match - if !search_forward then iit#forward_search txt + if !search_forward then iit#forward_search txt else let npi = iit#forward_chars (Glib.Utf8.length txt) in - match + match (npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset), - (let t = iit#get_text ~stop:npi in - !flash_info (t^"\n"^txt); + (let t = iit#get_text ~stop:npi in + flash_info (t^"\n"^txt); t = txt) - with - | true,true -> - (!flash_info "T,T";iit#backward_search txt) - | false,true -> !flash_info "F,T";Some (iit,npi) + with + | true,true -> + (flash_info "T,T";iit#backward_search txt) + | false,true -> flash_info "F,T";Some (iit,npi) | _,false -> (iit#backward_search txt) - with - | None -> + with + | None -> if !ready_to_wrap_search then begin ready_to_wrap_search := false; - !flash_info "Search wrapped"; - v#buffer#place_cursor + flash_info "Search wrapped"; + v#buffer#place_cursor (if !search_forward then v#buffer#start_iter else v#buffer#end_iter); search_f () end else begin - if !search_forward then !flash_info "Search at end" - else !flash_info "Search at start"; + if !search_forward then flash_info "Search at end" + else flash_info "Search at start"; ready_to_wrap_search := true end - | Some (start,stop) -> + | Some (start,stop) -> prerr_endline "search: before moving marks"; prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset)); prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset)); @@ -3415,105 +3115,49 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); v#scroll_to_mark `SEL_BOUND ) in - ignore (search_input#entry#event#connect#key_release + ignore (search_input#entry#event#connect#key_release ~callback: (fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin - let v = (get_current_view ()).view in - (match !start_of_search with - | None -> + let v = session_notebook#current_term.script in + (match !start_of_search with + | None -> prerr_endline "search_key_rel: Placing sel_bound"; - v#buffer#move_mark - `SEL_BOUND + v#buffer#move_mark + `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT) - | Some mk -> let it = v#buffer#get_iter_at_mark + | Some mk -> let it = v#buffer#get_iter_at_mark (`MARK mk) in prerr_endline "search_key_rel: Placing cursor"; v#buffer#place_cursor it; start_of_search := None ); - search_input#entry#set_text ""; + search_input#entry#set_text ""; v#coerce#misc#grab_focus (); - end; + end; false )); ignore (search_input#entry#connect#changed search_f); - - (* - ignore (search_if#connect#activate - ~callback:(fun b -> - search_forward:= true; - search_input#entry#coerce#misc#grab_focus (); - search_f (); - ) - ); - ignore (search_ib#connect#activate - ~callback:(fun b -> - search_forward:= false; - - (* Must restore the SEL_BOUND mark after - grab_focus ! *) - let v = (get_current_view ()).view in - let old_sel = v#buffer#get_iter_at_mark `SEL_BOUND - in - search_input#entry#coerce#misc#grab_focus (); - v#buffer#move_mark `SEL_BOUND old_sel; - search_f (); - )); - *) - let status_context = status_bar#new_context "Messages" in - let flash_context = status_bar#new_context "Flash" in - ignore (status_context#push "Ready"); - status := Some status_bar; - push_info := (fun s -> ignore (status_context#push s)); - pop_info := (fun () -> status_context#pop ()); - flash_info := (fun ?(delay=5000) s -> flash_context#flash ~delay s); - - (* Location display *) + push_info "Ready"; + (* Location display *) let l = GMisc.label - ~text:"Line: 1 Char: 1" - ~packing:lower_hbox#pack () in + ~text:"Line: 1 Char: 1" + ~packing:lower_hbox#pack () in l#coerce#misc#set_name "location"; set_location := l#set_text; - (* Progress Bar *) - pulse := - (let pb = GRange.progress_bar ~pulse_step:0.2 ~packing:lower_hbox#pack () - in pb#set_text "CoqIde started";pb)#pulse; - let tv2 = GText.view ~packing:(sw2#add) () in - tv2#misc#set_name "GoalWindow"; - let _ = tv2#set_editable false in - let _ = tv2#buffer in - let tv3 = GText.view ~packing:(sw3#add) () in - tv2#misc#set_name "MessageWindow"; - let _ = tv2#set_wrap_mode `CHAR in - let _ = tv3#set_wrap_mode `WORD in - let _ = tv3#set_editable false in - let _ = GtkBase.Widget.add_events tv2#as_widget - [`ENTER_NOTIFY;`POINTER_MOTION] in - let _ = - tv2#event#connect#motion_notify - ~callback: - (fun e -> - let win = match tv2#get_window `WIDGET with - | None -> assert false - | Some w -> w in - let x,y = Gdk.Window.get_pointer_location win in - let b_x,b_y = tv2#window_to_buffer_coords ~tag:`WIDGET ~x ~y in - let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in - let tags = it#tags in - List.iter - (fun t -> - ignore(GtkText.Tag.event t#as_tag tv2#as_widget e it#as_iter)) - tags; - false) in - change_font := - (fun fd -> - tv2#misc#modify_font fd; - tv3#misc#modify_font fd; - Vector.iter - (fun {view=view} -> view#misc#modify_font fd) - input_views; + lower_hbox#pack pbar#coerce; + pbar#set_text "CoqIde started"; + (* XXX *) + change_font := + (fun fd -> + List.iter + (fun {script=view; proof_view=prf_v; message_view=msg_v} -> + view#misc#modify_font fd; + prf_v#misc#modify_font fd; + msg_v#misc#modify_font fd + ) + session_notebook#pages; ); let about_full_string = "\nCoq is developed by the Coq Development Team\ @@ -3539,7 +3183,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); b#insert ~iter:b#start_iter "\n\n"; if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version); if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string; - (try + (try let image = lib_ide_file "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; @@ -3549,7 +3193,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in let about (b:GText.buffer) = - (try + (try let image = lib_ide_file "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; @@ -3563,77 +3207,30 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); 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: - (fun ev -> GdkEvent.Button.button ev = 3)); - ignore (tv3#event#connect#button_press ~callback: - (fun ev -> GdkEvent.Button.button ev = 3)); - tv2#misc#set_can_focus true; - tv3#misc#set_can_focus true; - ignore (tv2#buffer#create_mark - ~name:"end_of_conclusion" - tv2#buffer#start_iter); - ignore (tv3#buffer#create_tag - ~name:"error" - [`FOREGROUND "red"]); w#show (); - message_view := Some tv3; - proof_view := Some tv2; - tv2#misc#modify_font !current.text_font; - tv3#misc#modify_font !current.text_font; - ignore (about_m#connect#activate - ~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer)); + ignore (about_m#connect#activate + ~callback:(fun () -> let prf_v = session_notebook#current_term.proof_view in + prf_v#buffer#set_text ""; about prf_v#buffer)); (* - ignore (faq_m#connect#activate - ~callback:(fun () -> - load (lib_ide_file "FAQ"))); - + *) - resize_window := (fun () -> - w#resize + resize_window := (fun () -> + w#resize ~width:!current.window_width ~height:!current.window_height); - - ignore (w#misc#connect#size_allocate - (let old_w = ref 0 - and old_h = ref 0 in - fun {Gtk.width=w;Gtk.height=h} -> - if !old_w <> w or !old_h <> h then - begin - old_h := h; - old_w := w; - hb#set_position (w/2); - hb2#set_position (h/2); - !current.window_height <- h; - !current.window_width <- w; - end - )); - ignore(nb#connect#switch_page + ignore(nb#connect#switch_page ~callback: - (fun i -> + (fun i -> prerr_endline ("switch_page: starts " ^ string_of_int i); List.iter (function f -> f i) !to_do_on_page_switch; prerr_endline "switch_page: success") ); - ignore(tv2#event#connect#enter_notify - (fun _ -> - if !current.contextual_menus_on_goal then - begin - 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; - prerr_endline "....Done with Goal menu"; - !pop_info(); - end; - false; - )); - if List.length files >=1 then + if List.length files >=1 then begin - List.iter (fun f -> - if Sys.file_exists f then load f else + List.iter (fun f -> + if Sys.file_exists f then load f else 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; @@ -3641,69 +3238,66 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); end else begin - let view = create_input_tab "*Unnamed Buffer*" in - let index = add_input_view {view = view; - analyzed_view = None; - } - in - (get_input_view index).analyzed_view <- Some (new analyzed_view index); + let session = create_session () in + let index = session_notebook#append_term session in activate_input index; - set_tab_image index ~icon:`YES; - view#misc#modify_font !current.text_font end; + initial_about session_notebook#current_term.proof_view#buffer; + !show_toolbar !current.show_toolbar; + session_notebook#current_term.script#misc#grab_focus () ;; -(* This function check every half of second if GeoProof has send +(* This function check every half of second if GeoProof has send something on his private clipboard *) -let rec check_for_geoproof_input () = +let rec check_for_geoproof_input () = let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in while true do Thread.delay 0.1; let s = cb_Dr#text in - (match s with - Some s -> + (match s with + Some s -> if s <> "Ack" then - (get_current_view()).view#buffer#insert (s^"\n"); + session_notebook#current_term.script#buffer#insert (s^"\n"); cb_Dr#set_text "Ack" | None -> () ); (* cb_Dr#clear does not work so i use : *) - (* cb_Dr#set_text "Ack" *) + (* cb_Dr#set_text "Ack" *) done - - -let start () = + + +let start () = let files = Coq.init () in ignore_break (); GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); - (try + (try GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc"); with Not_found -> ()); ignore (GtkMain.Main.init ()); - GtkData.AccelGroup.set_default_mod_mask + GtkData.AccelGroup.set_default_mod_mask (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]); - cb_ := Some (GData.clipboard Gdk.Atom.primary); ignore ( Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL; `WARNING;`CRITICAL] - (fun ~level msg -> + (fun ~level msg -> if level land Glib.Message.log_level `WARNING <> 0 then Pp.warning msg 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 - try - GtkThread.main () + if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); + while true do + try + GtkThread.main () with | Sys.Break -> prerr_endline "Interrupted." ; flush stderr - | e -> + | e -> Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); flush stderr; crash_save 127 done + + diff --git a/ide/coqide.mli b/ide/coqide.mli index f904c730..4c01e747 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: coqide.mli 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id$ i*) (* The CoqIde main module. The following function [start] will parse the - command line, initialize the load path, load the input + command line, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch the interface. *) diff --git a/ide/extract_index.mll b/ide/extract_index.mll deleted file mode 100644 index 152ad715..00000000 --- a/ide/extract_index.mll +++ /dev/null @@ -1,31 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* " [^ ',']* ", " - { let s = lexeme lexbuf in - let n = String.length s in - String.sub s 8 (n - 15), extract_index_url lexbuf } - | "
  • " [^ ',']* ", " - { let s = lexeme lexbuf in - let n = String.length s in - String.sub s 4 (n - 6), extract_index_url lexbuf } - -and extract_index_url = parse - | "0 && is_word_char c then ( + ignore (it#nocopy#forward_char); + step_to_end it + ) else ( + prerr_endline ("Word end at: "^(string_of_int it#offset)); + it) + in + step_to_end it#copy + + +let get_word_around (it:GText.iter) = + let start = find_word_start it in + let stop = find_word_end it in + start,stop + + +let rec complete_backward w (it:GText.iter) = + prerr_endline "Complete backward..."; + match it#backward_search w with + | None -> (prerr_endline "backward_search failed";None) + | Some (start,stop) -> + prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset)); + if starts_word start then + let ne = find_word_end stop in + if ne#compare stop = 0 + then complete_backward w start + else Some (start,stop,ne) + else complete_backward w start + + +let rec complete_forward w (it:GText.iter) = + prerr_endline "Complete forward..."; + match it#forward_search w with + | None -> None + | Some (start,stop) -> + if starts_word start then + let ne = find_word_end stop in + if ne#compare stop = 0 then + complete_forward w stop + else Some (stop,stop,ne) + else complete_forward w stop + + +let find_comment_end (start:GText.iter) = + let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) = + match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with + | None,_ -> comment_end + | Some _, None -> raise Not_found + | Some (_,next_search_start),Some (next_search_end,next_comment_end) -> + find_nested_comment next_search_start next_search_end next_comment_end + in + match start#forward_search "*)" with + | None -> raise Not_found + | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end + + +let rec find_string_end (start:GText.iter) = + let dblquote = int_of_char '"' in + let rec escaped_dblquote c = + (c#char = dblquote) && not (escaped_dblquote c#backward_char) + in + match start#forward_search "\"" with + | None -> raise Not_found + | Some (stop,next_start) -> + if escaped_dblquote stop#backward_char + then find_string_end next_start + else next_start + + +let rec find_next_sentence (from:GText.iter) = + match (from#forward_search ".") with + | None -> raise Not_found + | Some (non_vernac_search_end,next_sentence) -> + match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with + | None,None -> + if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0 + then next_sentence else find_next_sentence next_sentence + | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start) + | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start) + | Some (_,comment_search_start),Some (_,string_search_start) -> + find_next_sentence ( + if comment_search_start#compare string_search_start < 0 + then find_comment_end comment_search_start + else find_string_end string_search_start) + + +let find_nearest_forward (cursor:GText.iter) targets = + let fold_targets acc target = + match cursor#forward_search target,acc with + | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start + | Some (t_start,_),None -> Some t_start + | _ -> acc + in + match List.fold_left fold_targets None targets with + | None -> raise Not_found + | Some nearest -> nearest + + +let find_nearest_backward (cursor:GText.iter) targets = + let fold_targets acc target = + match cursor#backward_search target,acc with + | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start + | Some (t_start,_),None -> Some t_start + | _ -> acc + in + match List.fold_left fold_targets None targets with + | None -> raise Not_found + | Some nearest -> nearest + diff --git a/ide/highlight.mll b/ide/highlight.mll index f2ecaa9c..3acdd4f0 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: highlight.mll 11481 2008-10-20 19:23:51Z herbelin $ *) +(* $Id$ *) { open Lexing - type color = string + type color = GText.tag type highlight_order = int * int * color @@ -24,7 +24,7 @@ let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) [ "Add" ; "Check"; "Eval"; "Extraction" ; - "Load" ; "Undo"; "Goal"; + "Load" ; "Undo"; "Goal"; "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ; "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]; @@ -33,9 +33,9 @@ let is_constr_kw = let h = Hashtbl.create 97 in 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" ]; + [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for"; + "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return"; + "Prop"; "Set"; "Type" ]; Hashtbl.mem h (* Without this table, the automaton would be too big and @@ -48,7 +48,7 @@ "Proposition" ; "Property" ; (* Definitions *) "Definition" ; "Let" ; "Example" ; "SubClass" ; - "Fixpoint" ; "CoFixpoint" ; "Scheme" ; + "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ; (* Assumptions *) "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ; "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters"; @@ -62,11 +62,11 @@ let starting = ref true } -let space = +let space = [' ' '\010' '\013' '\009' '\012'] -let firstchar = +let firstchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'] -let identchar = +let identchar = ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9'] let ident = firstchar identchar* @@ -79,8 +79,8 @@ let multiword_declaration = let locality = ("Local" space+)? let multiword_command = - "Set" (space+ ident)* -| "Unset" (space+ ident)* + "Set" (space+ ident)* +| "Unset" (space+ ident)* | "Open" space+ locality "Scope" | "Close" space+ locality "Scope" | "Bind" space+ "Scope" @@ -98,6 +98,11 @@ let multiword_command = | "Implicit" space+ "Arguments" | "Implicit" space+ ("Type"|"Types") | "Combined" space+ "Scheme" +| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"))| + ("Library"|"Inline"|"NoInline"|"Blacklist")) +| "Recursive" space+ "Extraction" (space+ "Library")? +| ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist") +| "Extract" space+ (("Inlined" space+) "Constant"| "Inductive") (* At least still missing: "Inline" + decl, variants of "Identity Coercion", variants of Print, Add, ... *) @@ -106,17 +111,17 @@ 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" } + { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl } | multiword_command - { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, "kwd" } - | ident as id + { starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd } + | ident as id { 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" + starting:=false; + if is_one_word_command id then + lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd else if is_one_word_declaration id then - lexeme_start lexbuf, lexeme_end lexbuf, "decl" + lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl else next_interior_order lexbuf end @@ -125,11 +130,11 @@ rule next_starting_order = parse | eof { raise End_of_file } and next_interior_order = parse - | "(*" + | "(*" { comment_start := lexeme_start lexbuf; comment lexbuf } - | ident as id + | ident as id { if is_constr_kw id then - lexeme_start lexbuf, lexeme_end lexbuf, "kwd" + lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd else next_interior_order lexbuf } | "." (" "|"\n"|"\t") { starting := true; next_starting_order lexbuf } @@ -137,42 +142,49 @@ and next_interior_order = parse | eof { raise End_of_file } and comment = parse - | "*)" { !comment_start,lexeme_end lexbuf,"comment" } + | "*)" { !comment_start,lexeme_end lexbuf,Tags.Script.comment } | "(*" { ignore (comment lexbuf); comment lexbuf } + | "\"" { string_in_comment lexbuf } | _ { comment lexbuf } | eof { raise End_of_file } +and string_in_comment = parse + | "\"\"" { string_in_comment lexbuf } + | "\"" { comment lexbuf } + | _ { string_in_comment lexbuf } + | eof { raise End_of_file } + { open Ideutils let highlighting = ref false - let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop = + 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" + if !highlighting then prerr_endline "Rejected highlight" else begin highlighting := true; prerr_endline "Highlighting slice now"; - input_buffer#remove_tag_by_name ~start ~stop "error"; - input_buffer#remove_tag_by_name ~start ~stop "kwd"; - input_buffer#remove_tag_by_name ~start ~stop "decl"; - input_buffer#remove_tag_by_name ~start ~stop "comment"; + input_buffer#remove_tag ~start ~stop Tags.Script.error; + input_buffer#remove_tag ~start ~stop Tags.Script.kwd; + input_buffer#remove_tag ~start ~stop Tags.Script.decl; + input_buffer#remove_tag ~start ~stop Tags.Script.comment; (try begin let offset = start#offset in let s = start#get_slice ~stop in let convert_pos = byte_offset_to_char_offset s in let lb = Lexing.from_string s in - try + try while true do 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 - input_buffer#apply_tag_by_name ~start ~stop o + input_buffer#apply_tag ~start ~stop o done with End_of_file -> () end @@ -181,22 +193,22 @@ and comment = parse end let highlight_current_line input_buffer = - try + try let i = get_insert input_buffer in highlight_slice input_buffer (i#set_line_offset 0) i with _ -> () - let highlight_around_current_line input_buffer = - try + let highlight_around_current_line input_buffer = + try let i = get_insert input_buffer in - highlight_slice input_buffer - (i#backward_lines 10) + highlight_slice input_buffer + (i#backward_lines 10) (ignore (i#nocopy#forward_lines 10);i) with _ -> () - - let highlight_all input_buffer = - try + + let highlight_all input_buffer = + try highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter with _ -> () diff --git a/ide/ide.mllib b/ide/ide.mllib new file mode 100644 index 00000000..63935db3 --- /dev/null +++ b/ide/ide.mllib @@ -0,0 +1,23 @@ +Okey +Config_file +Configwin_keys +Configwin_types +Configwin_messages +Configwin_ihm +Configwin +Editable_cells +Config_parser +Tags +Typed_notebook +Config_lexer +Utf8_convert +Preferences +Ideutils +Coq_lex +Gtk_parsing +Undo +Coq +Coq_commands +Coq_tactics +Command_windows +Coqide diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d9b5e572..14e80389 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml 11749 2009-01-05 14:01:04Z notin $ *) +(* $Id$ *) open Preferences @@ -15,15 +15,21 @@ exception Forbidden (* status bar and locations *) -let status = ref None -let push_info = ref (function s -> failwith "not ready") -let pop_info = ref (function s -> failwith "not ready") -let flash_info = ref (fun ?delay s -> failwith "not ready") +let status = GMisc.statusbar () + +let push_info,pop_info = + let status_context = status#new_context "Messages" in + (fun s -> ignore (status_context#push s)),status_context#pop + +let flash_info = + let flash_context = status#new_context "Flash" in + (fun ?(delay=5000) s -> flash_context#flash ~delay s) -let set_location = ref (function s -> failwith "not ready") -let pulse = ref (function () -> failwith "not ready") +let set_location = ref (function s -> failwith "not ready") + +let pbar = GRange.progress_bar ~pulse_step:0.2 () let debug = Flags.debug @@ -35,12 +41,12 @@ let prerr_string s = let lib_ide_file f = let coqlib = Envars.coqlib () in Filename.concat (Filename.concat coqlib "ide") f - + let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0 -let byte_offset_to_char_offset s byte_offset = +let byte_offset_to_char_offset s byte_offset = if (byte_offset < String.length s) then begin let count_delta = ref 0 in for i = 0 to byte_offset do @@ -62,19 +68,19 @@ let print_id id = prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id))) -let do_convert s = +let do_convert s = Utf8_convert.f (if Glib.Utf8.validate s then begin prerr_endline "Input is UTF-8";s end else - let from_loc () = + let from_loc () = let _,char_set = Glib.Convert.get_charset () in - !flash_info + flash_info ("Converting from locale ("^char_set^")"); Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s in - let from_manual () = - !flash_info + let from_manual () = + flash_info ("Converting from "^ !current.encoding_manual); Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual in @@ -84,30 +90,30 @@ let do_convert s = with _ -> from_manual () end else begin try - from_manual () + from_manual () with _ -> from_loc () end) -let try_convert s = +let try_convert s = try do_convert s - with _ -> + with _ -> "(* Fatal error: wrong encoding in input. Please choose a correct encoding in the preference panel.*)";; -let try_export file_name s = - try let s = +let try_export file_name s = + try let s = try if !current.encoding_use_utf8 then begin (prerr_endline "UTF-8 is enforced" ;s) end else if !current.encoding_use_locale then begin let is_unicode,char_set = Glib.Convert.get_charset () in - if is_unicode then - (prerr_endline "Locale is UTF-8" ;s) + if is_unicode then + (prerr_endline "Locale is UTF-8" ;s) else (prerr_endline ("Locale is "^char_set); Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s) - end else + end else (prerr_endline ("Manual charset is "^ !current.encoding_manual); Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s) with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s) @@ -131,16 +137,16 @@ let disconnect_auto_save_timer () = match !auto_save_timer with | Some id -> GMain.Timeout.remove id; auto_save_timer := None let highlight_timer = ref None -let set_highlight_timer f = - match !highlight_timer with - | None -> - revert_timer := - Some (GMain.Timeout.add ~ms:2000 +let set_highlight_timer f = + match !highlight_timer with + | None -> + revert_timer := + Some (GMain.Timeout.add ~ms:2000 ~callback:(fun () -> f (); highlight_timer := None; true)) - | Some id -> + | Some id -> GMain.Timeout.remove id; - revert_timer := - Some (GMain.Timeout.add ~ms:2000 + revert_timer := + Some (GMain.Timeout.add ~ms:2000 ~callback:(fun () -> f (); highlight_timer := None; true)) @@ -150,31 +156,31 @@ let init_stdout,read_stdout,clear_stdout = 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 () -> + (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 (); + (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 () -> + (fun () -> Format.pp_print_flush out_ft (); Buffer.clear out_buff) let last_dir = ref "" -let filter_all_files () = GFile.filter - ~name:"All" - ~patterns:["*"] () - -let filter_coq_files () = GFile.filter - ~name:"Coq source code" +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 = 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 ; @@ -183,8 +189,8 @@ let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = file_chooser#set_default_response `OPEN; ignore (file_chooser#set_current_folder !dir); begin match file_chooser#run () with - | `OPEN -> - begin + | `OPEN -> + begin file := file_chooser#filename; match !file with None -> () @@ -192,27 +198,27 @@ let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () = end | `DELETE_EVENT | `CANCEL -> () end ; - file_chooser#destroy (); + file_chooser#destroy (); !file let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = - let file = ref None in + 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 + (* 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 + | `SAVE -> + begin file := file_chooser#filename; match !file with None -> () @@ -220,7 +226,7 @@ let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () = end | `DELETE_EVENT | `CANCEL -> () end ; - file_chooser#destroy (); + file_chooser#destroy (); !file let find_tag_start (tag :GText.tag) (it:GText.iter) = @@ -237,7 +243,7 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) = () done; it -let find_tag_limits (tag :GText.tag) (it:GText.iter) = +let find_tag_limits (tag :GText.tag) (it:GText.iter) = (find_tag_start tag it , find_tag_stop tag it) (* explanations: Win32 threads won't work if events are produced @@ -245,16 +251,16 @@ let find_tag_limits (tag :GText.tag) (it:GText.iter) = case we must use GtkThread.async to push a callback in the main thread. Beware that the synchronus version may produce deadlocks. *) -let async = +let async = if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x) -let sync = +let sync = if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x) let mutex text f = let m = Mutex.create() in fun x -> if Mutex.try_lock m - then + then (try prerr_endline ("Got lock on "^text); f x; @@ -269,8 +275,8 @@ let mutex text f = ("Discarded call for "^text^": computations ongoing") -let stock_to_widget ?(size=`DIALOG) s = - let img = GMisc.image () +let stock_to_widget ?(size=`DIALOG) s = + let img = GMisc.image () in img#set_stock s; img#coerce @@ -290,12 +296,12 @@ let run_command f c = let ne = ref 0 in 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 + let r = try_convert (String.sub buff 0 !n) in f r; Buffer.add_string result r; - let r = try_convert (String.sub buffe 0 !ne) in + let r = try_convert (String.sub buffe 0 !ne) in f r; - Buffer.add_string result r + Buffer.add_string result r done; (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) @@ -306,46 +312,60 @@ let browse f url = f ("Could not execute\n\""^com^ "\"\ncheck your preferences for setting a valid browser command\n") +let doc_url () = + if !current.doc_url = use_default_doc_url || !current.doc_url = "" then + if Sys.file_exists + (String.sub Coq_config.localwwwrefman 7 + (String.length Coq_config.localwwwrefman - 7)) + then + Coq_config.localwwwrefman + else + Coq_config.wwwrefman + else !current.doc_url + let url_for_keyword = let ht = Hashtbl.create 97 in + lazy ( begin try - let cin = open_in (lib_ide_file "index_urls.txt") in + let cin = + try open_in (lib_ide_file "index_urls.txt") + with _ -> + let doc_url = doc_url () in + let n = String.length doc_url in + if n > 8 && String.sub doc_url 0 7 = "file://" then + open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt") + else + raise Exit + in try while true do let s = input_line cin in - try + try let i = String.index s ',' in let k = String.sub s 0 i in let u = String.sub s (i + 1) (String.length s - i - 1) in Hashtbl.add ht k u with _ -> - () + Printf.eprintf "Warning: Cannot parse documentation index file.\n"; + flush stderr done with End_of_file -> close_in cin with _ -> - () + Printf.eprintf "Warning: Cannot find documentation index file.\n"; + flush stderr end; - (Hashtbl.find ht : string -> string) + Hashtbl.find ht : string -> string) -let browse_keyword f text = - try let u = url_for_keyword text in browse f (!current.doc_url ^ u) - with Not_found -> f ("No documentation found for "^text) - - -let underscore = Glib.Utf8.to_unichar "_" (ref 0) - -let arobase = Glib.Utf8.to_unichar "@" (ref 0) -let prime = Glib.Utf8.to_unichar "'" (ref 0) -let bn = Glib.Utf8.to_unichar "\n" (ref 0) -let space = Glib.Utf8.to_unichar " " (ref 0) -let tab = Glib.Utf8.to_unichar "\t" (ref 0) +let browse_keyword f text = + try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) + with Not_found -> f ("No documentation found for \""^text^"\".\n") (* checks if two file names refer to the same (existing) file by - comparing their device and inode. + comparing their device and inode. It seems that under Windows, inode is always 0, so we cannot - accurately check if + accurately check if *) (* Optimised for partial application (in case many candidates must be @@ -357,7 +377,7 @@ let same_file f1 = try let s2 = Unix.stat f2 in s1.Unix.st_dev = s2.Unix.st_dev && - if Sys.os_type = "Win32" then f1 = f2 + if Sys.os_type = "Win32" then f1 = f2 else s1.Unix.st_ino = s2.Unix.st_ino with Unix.Unix_error _ -> false) @@ -365,7 +385,7 @@ let same_file f1 = Unix.Unix_error _ -> (fun _ -> false) let absolute_filename f = - if Filename.is_relative f then + if Filename.is_relative f then Filename.concat (Sys.getcwd ()) f else f - + diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 48ff0fca..fbd5af44 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 11006 2008-05-28 10:42:45Z jnarboux $ i*) +(*i $Id$ i*) val async : ('a -> unit) -> 'a -> unit val sync : ('a -> 'b) -> 'a -> 'b @@ -14,6 +14,7 @@ val sync : ('a -> 'b) -> 'a -> 'b (* avoid running two instances of a function concurrently *) val mutex : string -> ('a -> unit) -> 'a -> unit +val doc_url : unit -> string val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int @@ -57,22 +58,15 @@ val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit val run_command : (string -> unit) -> string -> Unix.process_status*string -val prime : Glib.unichar -val underscore : Glib.unichar -val arobase : Glib.unichar -val bn : Glib.unichar -val space : Glib.unichar -val tab : Glib.unichar - -val status : GMisc.statusbar option ref -val push_info : (string -> unit) ref -val pop_info : (unit -> unit) ref -val flash_info : (?delay:int -> string -> unit) ref +val status : GMisc.statusbar +val push_info : string -> unit +val pop_info : unit -> unit +val flash_info : ?delay:int -> string -> unit val set_location : (string -> unit) ref -val pulse : (unit -> unit) ref +val pbar : GRange.progress_bar (* diff --git a/ide/preferences.ml b/ide/preferences.ml index ffb346d9..4e87d1df 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: preferences.ml 12104 2009-04-24 18:10:10Z notin $ *) +(* $Id$ *) open Configwin open Printf @@ -16,7 +16,7 @@ let pref_file = Filename.concat System.home ".coqiderc" let accel_file = Filename.concat System.home ".coqide.keys" -let mod_to_str (m:Gdk.Tags.modifier) = +let mod_to_str (m:Gdk.Tags.modifier) = match m with | `MOD1 -> "MOD1" | `MOD2 -> "MOD2" @@ -34,19 +34,19 @@ let mod_to_str (m:Gdk.Tags.modifier) = let (str_to_mod:string -> Gdk.Tags.modifier) = function - | "MOD1" -> `MOD1 - | "MOD2" -> `MOD2 - | "MOD3" -> `MOD3 - | "MOD4" -> `MOD4 - | "MOD5" -> `MOD5 - | "BUTTON1" -> `BUTTON1 - | "BUTTON2" -> `BUTTON2 - | "BUTTON3" -> `BUTTON3 - | "BUTTON4" -> `BUTTON4 - | "BUTTON5" -> `BUTTON5 - | "CONTROL" -> `CONTROL - | "LOCK" -> `LOCK - | "SHIFT" -> `SHIFT + | "MOD1" -> `MOD1 + | "MOD2" -> `MOD2 + | "MOD3" -> `MOD3 + | "MOD4" -> `MOD4 + | "MOD5" -> `MOD5 + | "BUTTON1" -> `BUTTON1 + | "BUTTON2" -> `BUTTON2 + | "BUTTON3" -> `BUTTON3 + | "BUTTON4" -> `BUTTON4 + | "BUTTON5" -> `BUTTON5 + | "CONTROL" -> `CONTROL + | "LOCK" -> `LOCK + | "SHIFT" -> `SHIFT | s -> `MOD1 type pref = @@ -100,7 +100,9 @@ type pref = mutable opposite_tabs : bool; } -let (current:pref ref) = +let use_default_doc_url = "(automatic)" + +let (current:pref ref) = ref { cmd_coqc = "coqc"; cmd_make = "make"; @@ -110,38 +112,38 @@ let (current:pref ref) = global_auto_revert = false; global_auto_revert_delay = 10000; - + auto_save = true; auto_save_delay = 10000; auto_save_name = "#","#"; - + encoding_use_locale = true; encoding_use_utf8 = false; encoding_manual = "ISO_8859-1"; automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ]; - + 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 = 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 "Monospace 10"; doc_url = Coq_config.wwwrefman; library_url = Coq_config.wwwstdlib; - + show_toolbar = true; contextual_menus_on_goal = true; window_width = 800; - window_height = 600; + window_height = 600; query_window_width = 600; query_window_height = 400; (* @@ -166,10 +168,10 @@ let contextual_menus_on_goal = ref (fun x -> ()) let resize_window = ref (fun () -> ()) let save_pref () = - (try GtkData.AccelMap.save accel_file + (try GtkData.AccelMap.save accel_file with _ -> ()); let p = !current in - try + try let add = Stringmap.add in let (++) x f = f x in Stringmap.empty ++ @@ -178,7 +180,7 @@ let save_pref () = add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ add "cmd_coqdoc" [p.cmd_coqdoc] ++ add "global_auto_revert" [string_of_bool p.global_auto_revert] ++ - add "global_auto_revert_delay" + add "global_auto_revert_delay" [string_of_int p.global_auto_revert_delay] ++ add "auto_save" [string_of_bool p.auto_save] ++ add "auto_save_delay" [string_of_int p.auto_save_delay] ++ @@ -190,15 +192,15 @@ let save_pref () = add "automatic_tactics" p.automatic_tactics ++ add "cmd_print" [p.cmd_print] ++ - add "modifier_for_navigation" + add "modifier_for_navigation" (List.map mod_to_str p.modifier_for_navigation) ++ - add "modifier_for_templates" + add "modifier_for_templates" (List.map mod_to_str p.modifier_for_templates) ++ - add "modifier_for_tactics" + add "modifier_for_tactics" (List.map mod_to_str p.modifier_for_tactics) ++ - add "modifier_for_display" + add "modifier_for_display" (List.map mod_to_str p.modifier_for_display) ++ - add "modifiers_valid" + add "modifiers_valid" (List.map mod_to_str p.modifiers_valid) ++ add "cmd_browse" [p.cmd_browse] ++ add "cmd_editor" [p.cmd_editor] ++ @@ -208,7 +210,7 @@ let save_pref () = add "doc_url" [p.doc_url] ++ add "library_url" [p.library_url] ++ add "show_toolbar" [string_of_bool p.show_toolbar] ++ - add "contextual_menus_on_goal" + add "contextual_menus_on_goal" [string_of_bool p.contextual_menus_on_goal] ++ add "window_height" [string_of_int p.window_height] ++ add "window_width" [string_of_int p.window_width] ++ @@ -221,12 +223,11 @@ let save_pref () = add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." - let load_pref () = (try GtkData.AccelMap.load accel_file with _ -> ()); - let p = !current in - try + let p = !current in + try let m = Config_lexer.load_file pref_file in let np = { p with cmd_coqc = p.cmd_coqc } in let set k f = try let v = Stringmap.find k m in f v with _ -> () in @@ -234,7 +235,7 @@ 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 = + 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); @@ -242,7 +243,7 @@ let load_pref () = set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v); set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v); - set_int "global_auto_revert_delay" + set_int "global_auto_revert_delay" (fun v -> np.global_auto_revert_delay <- v); set_bool "auto_save" (fun v -> np.auto_save <- v); set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v); @@ -253,23 +254,26 @@ let load_pref () = set "automatic_tactics" (fun v -> np.automatic_tactics <- v); set_hd "cmd_print" (fun v -> np.cmd_print <- v); - set "modifier_for_navigation" + set "modifier_for_navigation" (fun v -> np.modifier_for_navigation <- List.map str_to_mod v); - set "modifier_for_templates" + set "modifier_for_templates" (fun v -> np.modifier_for_templates <- List.map str_to_mod v); - set "modifier_for_tactics" + set "modifier_for_tactics" (fun v -> np.modifier_for_tactics <- List.map str_to_mod v); - set "modifier_for_display" + set "modifier_for_display" (fun v -> np.modifier_for_display <- List.map str_to_mod v); - set "modifiers_valid" + set "modifiers_valid" (fun v -> np.modifiers_valid <- List.map str_to_mod v); 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 "doc_url" (fun v -> + if not (Flags.is_standard_doc_url v) && v <> use_default_doc_url then + prerr_endline ("Warning: Non-standard URL for Coq documentation in preference file: "^v); + np.doc_url <- v); set_hd "library_url" (fun v -> np.library_url <- v); set_bool "show_toolbar" (fun v -> np.show_toolbar <- v); - set_bool "contextual_menus_on_goal" + set_bool "contextual_menus_on_goal" (fun v -> np.contextual_menus_on_goal <- v); set_int "window_width" (fun v -> np.window_width <- v); set_int "window_height" (fun v -> np.window_height <- v); @@ -284,38 +288,38 @@ let load_pref () = (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - with e -> + with e -> prerr_endline ("Could not load preferences ("^ (Printexc.to_string e)^").") - + let split_string_format s = - try + try let i = Util.string_index_from s 0 "%s" in let pre = (String.sub s 0 i) in let post = String.sub s (i+2) (String.length s - i - 2) in pre,post with Not_found -> s,"" -let configure ?(apply=(fun () -> ())) () = - let cmd_coqc = +let configure ?(apply=(fun () -> ())) () = + let cmd_coqc = string - ~f:(fun s -> !current.cmd_coqc <- s) + ~f:(fun s -> !current.cmd_coqc <- s) " coqc" !current.cmd_coqc in - let cmd_make = - string + let cmd_make = + string ~f:(fun s -> !current.cmd_make <- s) " make" !current.cmd_make in - let cmd_coqmakefile = - string + let cmd_coqmakefile = + string ~f:(fun s -> !current.cmd_coqmakefile <- s) "coqmakefile" !current.cmd_coqmakefile in - let cmd_coqdoc = - string + let cmd_coqdoc = + string ~f:(fun s -> !current.cmd_coqdoc <- s) " coqdoc" !current.cmd_coqdoc in - let cmd_print = - string - ~f:(fun s -> !current.cmd_print <- s) + let cmd_print = + string + ~f:(fun s -> !current.cmd_print <- s) " Print ps" !current.cmd_print in let config_font = @@ -324,15 +328,15 @@ let configure ?(apply=(fun () -> ())) () = w#set_preview_text "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; box#pack w#coerce; - ignore (w#misc#connect#realize - ~callback:(fun () -> w#set_font_name + ignore (w#misc#connect#realize + ~callback:(fun () -> w#set_font_name (Pango.Font.to_string !current.text_font))); custom ~label:"Fonts for text" box - (fun () -> + (fun () -> let fd = w#font_name in - !current.text_font <- (Pango.Font.from_string fd) ; + !current.text_font <- (Pango.Font.from_string fd) ; (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) @@ -340,80 +344,80 @@ let configure ?(apply=(fun () -> ())) () = true in (* - let show_toolbar = - bool - ~f:(fun s -> - !current.show_toolbar <- s; - !show_toolbar s) + let show_toolbar = + bool + ~f:(fun s -> + !current.show_toolbar <- s; + !show_toolbar s) "Show toolbar" !current.show_toolbar in let window_height = string ~f:(fun s -> !current.window_height <- (try int_of_string s with _ -> 600); !resize_window (); - ) - "Window height" + ) + "Window height" (string_of_int !current.window_height) - in + in let window_width = string - ~f:(fun s -> !current.window_width <- - (try int_of_string s with _ -> 800)) - "Window width" + ~f:(fun s -> !current.window_width <- + (try int_of_string s with _ -> 800)) + "Window width" (string_of_int !current.window_width) - in + in *) - let auto_complete = - bool - ~f:(fun s -> - !current.auto_complete <- s; - !auto_complete s) + let auto_complete = + bool + ~f:(fun s -> + !current.auto_complete <- s; + !auto_complete s) "Auto Complete" !current.auto_complete in -(* let use_utf8_notation = - bool - ~f:(fun b -> +(* let use_utf8_notation = + bool + ~f:(fun b -> !current.use_utf8_notation <- b; - ) + ) "Use Unicode Notation: " !current.use_utf8_notation in -*) +*) (* let config_appearance = [show_toolbar; window_width; window_height] in *) - let global_auto_revert = - bool - ~f:(fun s -> !current.global_auto_revert <- s) + let global_auto_revert = + bool + ~f:(fun s -> !current.global_auto_revert <- s) "Enable global auto revert" !current.global_auto_revert in let global_auto_revert_delay = string - ~f:(fun s -> !current.global_auto_revert_delay <- - (try int_of_string s with _ -> 10000)) - "Global auto revert delay (ms)" + ~f:(fun s -> !current.global_auto_revert_delay <- + (try int_of_string s with _ -> 10000)) + "Global auto revert delay (ms)" (string_of_int !current.global_auto_revert_delay) - in + in - let auto_save = - bool - ~f:(fun s -> !current.auto_save <- s) + let auto_save = + bool + ~f:(fun s -> !current.auto_save <- s) "Enable auto save" !current.auto_save in let auto_save_delay = string - ~f:(fun s -> !current.auto_save_delay <- - (try int_of_string s with _ -> 10000)) - "Auto save delay (ms)" + ~f:(fun s -> !current.auto_save_delay <- + (try int_of_string s with _ -> 10000)) + "Auto save delay (ms)" (string_of_int !current.auto_save_delay) - in + in let stop_before = bool ~f:(fun s -> !current.stop_before <- s) "Stop interpreting before the current point" !current.stop_before in - + let lax_syntax = bool ~f:(fun s -> !current.lax_syntax <- s) @@ -432,31 +436,31 @@ let configure ?(apply=(fun () -> ())) () = "Tabs on opposite side" !current.opposite_tabs in - let encodings = - combo + let encodings = + combo "File charset encoding " - ~f:(fun s -> + ~f:(fun s -> match s with - | "UTF-8" -> + | "UTF-8" -> !current.encoding_use_utf8 <- true; !current.encoding_use_locale <- false | "LOCALE" -> !current.encoding_use_utf8 <- false; !current.encoding_use_locale <- true - | _ -> + | _ -> !current.encoding_use_utf8 <- false; !current.encoding_use_locale <- false; !current.encoding_manual <- s; ) ~new_allowed: true ["UTF-8";"LOCALE";!current.encoding_manual] - (if !current.encoding_use_utf8 then "UTF-8" + (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!)" + let help_string = + "restart to apply" in - let modifier_for_tactics = + let modifier_for_tactics = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_tactics <- l) @@ -464,7 +468,7 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Tactics Menu" !current.modifier_for_tactics in - let modifier_for_templates = + let modifier_for_templates = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_templates <- l) @@ -472,7 +476,7 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Templates Menu" !current.modifier_for_templates in - let modifier_for_navigation = + let modifier_for_navigation = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_navigation <- l) @@ -480,7 +484,7 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Navigation Menu" !current.modifier_for_navigation in - let modifier_for_display = + let modifier_for_display = modifiers ~allow:!current.modifiers_valid ~f:(fun l -> !current.modifier_for_display <- l) @@ -488,23 +492,23 @@ let configure ?(apply=(fun () -> ())) () = "Modifiers for Display Menu" !current.modifier_for_display in - let modifiers_valid = + let modifiers_valid = modifiers ~f:(fun l -> !current.modifiers_valid <- l) "Allowed modifiers" !current.modifiers_valid in - let cmd_editor = + let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo - ~help:"(%s for file name)" + ~help:"(%s for file name)" "External 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 + in let cmd_browse = let predefined = [ Coq_config.browser; @@ -514,40 +518,57 @@ let configure ?(apply=(fun () -> ())) () = "seamonkey -remote \"openURL(%s)\" || seamonkey %s &"; "open -a Safari %s &" ] in - combo - ~help:"(%s for url)" + combo + ~help:"(%s for url)" "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 - let library_url = - string ~f:(fun s -> !current.library_url <- s) "Library URL" !current.library_url in - - let automatic_tactics = + in + let doc_url = + let predefined = [ + use_default_doc_url + ] in + combo + "Manual URL" + ~f:(fun s -> !current.doc_url <- s) + ~new_allowed: true + (predefined@[if List.mem !current.doc_url predefined then "" + else !current.doc_url]) + !current.doc_url in + let library_url = + let predefined = [ + Coq_config.wwwstdlib + ] in + combo + "Library URL" + ~f:(fun s -> !current.library_url <- s) + (predefined@[if List.mem !current.library_url predefined then "" + else !current.library_url]) + !current.library_url + in + let automatic_tactics = strings - ~f:(fun l -> !current.automatic_tactics <- l) + ~f:(fun l -> !current.automatic_tactics <- l) ~add:(fun () -> [""]) - "Wizard tactics to try in order" + "Wizard tactics to try in order" !current.automatic_tactics in let contextual_menus_on_goal = - bool - ~f:(fun s -> - !current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal s) + bool + ~f:(fun s -> + !current.contextual_menus_on_goal <- s; + !contextual_menus_on_goal s) "Contextual menus on goal" !current.contextual_menus_on_goal - in + 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) *) let cmds = @@ -557,7 +578,7 @@ let configure ?(apply=(fun () -> ())) () = [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) encodings; - ]); + ]); (* Section("Appearance", config_appearance); @@ -581,6 +602,6 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - match x with + match x with | Return_apply | Return_ok -> save_pref () | Return_cancel -> () diff --git a/ide/preferences.mli b/ide/preferences.mli index d7f32380..6ee7918f 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 11009 2008-05-28 13:58:33Z jnarboux $ i*) +(*i $Id$ i*) type pref = { @@ -70,3 +70,5 @@ val change_font : ( Pango.font_description -> unit) ref val show_toolbar : (bool -> unit) ref val auto_complete : (bool -> unit) ref val resize_window : (unit -> unit) ref + +val use_default_doc_url : string diff --git a/ide/tags.ml b/ide/tags.ml new file mode 100644 index 00000000..e78f5c82 --- /dev/null +++ b/ide/tags.ml @@ -0,0 +1,50 @@ + +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(*