diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 11 | ||||
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coqOps.ml | 54 | ||||
| -rw-r--r-- | ide/coqOps.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 1 | ||||
| -rw-r--r-- | ide/ide_slave.ml | 24 | ||||
| -rw-r--r-- | ide/ideutils.ml | 52 | ||||
| -rw-r--r-- | ide/ideutils.mli | 2 | ||||
| -rw-r--r-- | ide/preferences.ml | 46 | ||||
| -rw-r--r-- | ide/preferences.mli | 2 | ||||
| -rw-r--r-- | ide/sentence.ml | 1 | ||||
| -rw-r--r-- | ide/session.ml | 14 | ||||
| -rw-r--r-- | ide/tags.ml | 7 | ||||
| -rw-r--r-- | ide/tags.mli | 2 | ||||
| -rw-r--r-- | ide/texmacspp.ml | 7 | ||||
| -rw-r--r-- | ide/wg_MessageView.ml | 9 | ||||
| -rw-r--r-- | ide/xml_printer.ml | 116 | ||||
| -rw-r--r-- | ide/xmlprotocol.ml | 32 | ||||
| -rw-r--r-- | ide/xmlprotocol.mli | 4 |
19 files changed, 242 insertions, 146 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 61f002576b..6d44ca59e3 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -227,7 +227,7 @@ type coqtop = { (* non quoted command-line arguments of coqtop *) mutable sup_args : string list; (* called whenever coqtop dies *) - mutable reset_handler : reset_kind -> unit task; + mutable reset_handler : unit task; (* called whenever coqtop sends a feedback message *) mutable feedback_handler : Feedback.feedback -> unit; (* actual coqtop process and its status *) @@ -298,7 +298,7 @@ let handle_intermediate_message handle level content = | Feedback.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) | Feedback.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) | Feedback.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) - | Feedback.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) + | Feedback.Debug -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) in logger level content @@ -333,7 +333,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; match Xmlprotocol.is_message xml with - | Some (lvl, msg) -> + | Some (lvl, _loc, msg) -> handle_intermediate_message handle lvl msg; loop () | None -> @@ -421,6 +421,7 @@ let mkready coqtop = fun () -> coqtop.status <- Ready; Void let rec respawn_coqtop ?(why=Unexpected) coqtop = + if why = Unexpected then warning "Coqtop died badly. Resetting."; clear_handle coqtop.handle; ignore_error (fun () -> coqtop.handle <- @@ -432,7 +433,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop = If not, there isn't much we can do ... *) assert (coqtop.handle.alive = true); coqtop.status <- New; - ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop)) + ignore (coqtop.reset_handler coqtop.handle (mkready coqtop)) let spawn_coqtop sup_args = bind_self_as (fun this -> { @@ -440,7 +441,7 @@ let spawn_coqtop sup_args = (fun () -> respawn_coqtop (this ())) (fun msg -> (this ()).feedback_handler msg); sup_args = sup_args; - reset_handler = (fun _ _ k -> k ()); + reset_handler = (fun _ k -> k ()); feedback_handler = (fun _ -> ()); status = New; }) diff --git a/ide/coq.mli b/ide/coq.mli index 7cef6a4d0a..8a1fa3ed15 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -60,7 +60,7 @@ val is_computing : coqtop -> bool val spawn_coqtop : string list -> coqtop (** Create a coqtop process with some command-line arguments. *) -val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit +val set_reset_handler : coqtop -> unit task -> unit (** Register a handler called when a coqtop dies (badly or on purpose) *) val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 6ffe771da3..1563c7ffb4 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -14,15 +14,17 @@ open Feedback let b2c = byte_offset_to_char_offset -type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string ] -type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ] +type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ] +type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ] let mem_flag_of_flag : flag -> mem_flag = function | `ERROR _ -> `ERROR + | `WARNING _ -> `WARNING | (`INCOMPLETE | `UNSAFE | `PROCESSING) as mem_flag -> mem_flag let str_of_flag = function | `UNSAFE -> "U" | `PROCESSING -> "P" | `ERROR _ -> "E" + | `WARNING _ -> "W" | `INCOMPLETE -> "I" class type signals = @@ -136,7 +138,7 @@ object method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task - method handle_reset_initial : Coq.reset_kind -> unit task + method handle_reset_initial : unit task method raw_coq_query : string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task @@ -337,8 +339,11 @@ object(self) method private show_goals_aux ?(move_insert=false) () = Coq.PrintOpt.set_printing_width proof#width; if move_insert then begin - buffer#place_cursor ~where:self#get_start_of_input; - script#recenter_insert; + let dest = self#get_start_of_input in + if (buffer#get_iter_at_mark `INSERT)#compare dest <= 0 then begin + buffer#place_cursor ~where:dest; + script#recenter_insert + end end; Coq.bind (Coq.goals ~logger:messages#push ()) (function | Fail x -> self#handle_failure_aux ~move_insert x @@ -442,7 +447,6 @@ object(self) | Processed, Some (id,sentence) -> log "Processed" id; remove_flag sentence `PROCESSING; - remove_flag sentence `ERROR; self#mark_as_needed sentence | ProcessingIn _, Some (id,sentence) -> log "ProcessingIn" id; @@ -460,7 +464,9 @@ object(self) log "GlobRef" id; self#attach_tooltip sentence loc (Printf.sprintf "%s %s %s" filepath ident ty) - | ErrorMsg(loc, msg), Some (id,sentence) -> + | Message(Error, loc, msg), Some (id,sentence) -> + let loc = Option.default Loc.ghost loc in + let msg = Richpp.raw_print msg in log "ErrorMsg" id; remove_flag sentence `PROCESSING; add_flag sentence (`ERROR (loc, msg)); @@ -468,6 +474,15 @@ object(self) self#attach_tooltip sentence loc msg; if not (Loc.is_ghost loc) then self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc)) + | Message(Warning, loc, msg), Some (id,sentence) -> + let loc = Option.default Loc.ghost loc in + let msg = Richpp.raw_print msg in + log "WarningMsg" id; + add_flag sentence (`WARNING (loc, msg)); + self#attach_tooltip sentence loc msg; + self#position_warning_tag_at_sentence sentence loc + | Message((Info|Notice|Debug as lvl), _, msg), _ -> + messages#push lvl msg | InProgress n, _ -> if n < 0 then processed <- processed + abs n else to_process <- to_process + n @@ -509,6 +524,18 @@ object(self) let start, _, phrase = self#get_sentence sentence in self#position_error_tag_at_iter start phrase loc + method private position_warning_tag_at_iter iter_start iter_stop phrase loc = + if Loc.is_ghost loc then + buffer#apply_tag Tags.Script.warning ~start:iter_start ~stop:iter_stop + else + buffer#apply_tag Tags.Script.warning + ~start:(iter_start#forward_chars (b2c phrase loc.Loc.bp)) + ~stop:(iter_stop#forward_chars (b2c phrase loc.Loc.ep)) + + method private position_warning_tag_at_sentence sentence loc = + let start, stop, phrase = self#get_sentence sentence in + self#position_warning_tag_at_iter start stop phrase loc + method private process_interp_error queue sentence loc msg tip id = Coq.bind (Coq.return ()) (function () -> let start, stop, phrase = self#get_sentence sentence in @@ -535,13 +562,19 @@ object(self) condition returns true; it is fed with the number of phrases read and the iters enclosing the current sentence. *) method private fill_command_queue until queue = + let topstack = + if Doc.focused document then fst (Doc.context document) else [] in let rec loop n iter = match Sentence.find buffer iter with | None -> () | Some (start, stop) -> if until n start stop then begin () - end else if stop#backward_char#has_tag Tags.Script.processed then begin + end else if + List.exists (fun (_, s) -> + start#equal (buffer#get_iter_at_mark s.start) && + stop#equal (buffer#get_iter_at_mark s.stop)) topstack + then begin Queue.push (`Skip (start, stop)) queue; loop n stop end else begin @@ -759,7 +792,6 @@ object(self) method private handle_failure_aux ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = - messages#clear; messages#push Feedback.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) @@ -842,10 +874,8 @@ object(self) in loop l - method handle_reset_initial why = + method handle_reset_initial = let action () = - if why = Coq.Unexpected then warning "Coqtop died badly. Resetting." - else (* clear the stack *) if Doc.focused document then Doc.unfocus document; while not (Doc.is_empty document) do diff --git a/ide/coqOps.mli b/ide/coqOps.mli index 4a37a1fa55..332c18f2f0 100644 --- a/ide/coqOps.mli +++ b/ide/coqOps.mli @@ -15,7 +15,7 @@ object method tactic_wizard : string list -> unit task method process_next_phrase : unit task method process_until_end_or_error : unit task - method handle_reset_initial : Coq.reset_kind -> unit task + method handle_reset_initial : unit task method raw_coq_query : string -> unit task method show_goals : unit task method backtrack_last_phrase : unit task diff --git a/ide/coqide.ml b/ide/coqide.ml index d1a799a773..450bfcdfb1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -937,7 +937,6 @@ let emit_to_focus window sgn = let build_ui () = let w = GWindow.window ~wm_class:"CoqIde" ~wm_name:"CoqIde" - ~allow_grow:true ~allow_shrink:true ~width:window_width#get ~height:window_height#get ~title:"CoqIde" () in diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 9f10b2502a..5b07d3ec3b 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -8,7 +8,7 @@ (************************************************************************) open Vernacexpr -open Errors +open CErrors open Util open Pp open Printer @@ -96,11 +96,11 @@ let is_undo cmd = match cmd with (** Check whether a command is forbidden by CoqIDE *) let coqide_cmd_checks (loc,ast) = - let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in + let user_error s = CErrors.user_err_loc (loc, "CoqIde", str s) in if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then @@ -300,7 +300,7 @@ let dirpath_of_string_list s = let id = try Nametab.full_name_module qid with Not_found -> - Errors.errorlabstrm "Search.interface_search" + CErrors.errorlabstrm "Search.interface_search" (str "Module " ++ str path ++ str " not found.") in id @@ -365,12 +365,12 @@ let handle_exn (e, info) = | _ -> None in let mk_msg () = let msg = read_stdout () in - let msg = str msg ++ fnl () ++ Errors.print ~info e in + let msg = str msg ++ fnl () ++ CErrors.print ~info e in Richpp.richpp_of_pp msg in match e with - | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" - | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" + | CErrors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!" + | CErrors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () @@ -469,14 +469,14 @@ let print_xml = fun oc xml -> Mutex.lock m; try Xml_printer.print oc xml; Mutex.unlock m - with e -> let e = Errors.push e in Mutex.unlock m; iraise e + with e -> let e = CErrors.push e in Mutex.unlock m; iraise e -let slave_logger xml_oc level message = +let slave_logger xml_oc ?loc level message = (* convert the message into XML *) let msg = hov 0 message in - let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in - let xml = Xmlprotocol.of_message level (Richpp.richpp_of_pp message) in + let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in + let xml = Xmlprotocol.of_message level loc (Richpp.richpp_of_pp message) in print_xml xml_oc xml let slave_feeder xml_oc msg = @@ -499,7 +499,7 @@ let loop () = let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in let () = Xml_parser.check_eof xml_ic false in Feedback.set_logger (slave_logger xml_oc); - Feedback.set_feeder (slave_feeder xml_oc); + Feedback.add_feeder (slave_feeder xml_oc); (* We'll handle goal fetching and display in our own way *) Vernacentries.enable_goal_printing := false; Vernacentries.qed_display_script := false; diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 00c3f88e56..06a1327320 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -46,23 +46,37 @@ let xml_to_string xml = let () = iter (Richpp.repr xml) in Buffer.contents buf -let translate s = s - -let insert_xml ?(tags = []) (buf : #GText.buffer_skel) msg = +let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text = + (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that + it has to reimplement its own helper function. Unluckily, it relies on + a slow algorithm, so that we have to have our own quicker version here. + Alas, it is still much slower than the native version... *) + if CList.is_empty tags then buf#insert ~iter:(buf#get_iter_at_mark mark) text + else + let it = buf#get_iter_at_mark mark in + let () = buf#move_mark rmark ~where:it in + let () = buf#insert ~iter:(buf#get_iter_at_mark mark) text in + let start = buf#get_iter_at_mark mark in + let stop = buf#get_iter_at_mark rmark in + let iter tag = buf#apply_tag tag start stop in + List.iter iter tags + +let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let open Xml_datatype in let tag name = - let name = translate name in match GtkText.TagTable.lookup buf#tag_table name with | None -> raise Not_found | Some tag -> new GText.tag tag in + let rmark = `MARK (buf#create_mark buf#start_iter) in let rec insert tags = function - | PCData s -> buf#insert ~tags:(List.rev tags) s + | PCData s -> insert_with_tags buf mark rmark tags s | Element (t, _, children) -> let tags = try tag t :: tags with Not_found -> tags in List.iter (fun xml -> insert tags xml) children in - insert tags (Richpp.repr msg) + let () = try insert tags (Richpp.repr msg) with _ -> () in + buf#delete_mark rmark let set_location = ref (function s -> failwith "not ready") @@ -112,6 +126,24 @@ let try_convert s = "(* Fatal error: wrong encoding in input. \ Please choose a correct encoding in the preference panel.*)";; +let export file_name s = + let oc = open_out_bin file_name in + let ending = line_ending#get in + let is_windows = ref false in + for i = 0 to String.length s - 1 do + match s.[i] with + | '\r' -> is_windows := true + | '\n' -> + begin match ending with + | `DEFAULT -> + if !is_windows then (output_char oc '\r'; output_char oc '\n') + else output_char oc '\n' + | `WINDOWS -> output_char oc '\r'; output_char oc '\n' + | `UNIX -> output_char oc '\n' + end + | c -> output_char oc c + done; + close_out oc let try_export file_name s = let s = @@ -134,11 +166,7 @@ let try_export file_name s = Minilib.log ("Error ("^str^") in transcoding: falling back to UTF-8"); s in - try - let oc = open_out file_name in - output_string oc s; - close_out oc; - true + try export file_name s; true with e -> Minilib.log (Printexc.to_string e);false type timer = { run : ms:int -> callback:(unit->bool) -> unit; @@ -301,7 +329,7 @@ type logger = Feedback.level -> Richpp.richpp -> unit let default_logger level message = let level = match level with - | Feedback.Debug _ -> `DEBUG + | Feedback.Debug -> `DEBUG | Feedback.Info -> `INFO | Feedback.Notice -> `NOTICE | Feedback.Warning -> `WARNING diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 491e8e823d..e32a4d9e38 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -54,7 +54,7 @@ val flash_info : ?delay:int -> string -> unit val xml_to_string : Richpp.richpp -> string -val insert_xml : ?tags:GText.tag list -> +val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit val set_location : (string -> unit) ref diff --git a/ide/preferences.ml b/ide/preferences.ml index 3a33bbb1d8..f0fd45d77f 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -33,6 +33,7 @@ type obj = { } let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty +let unknown_preferences : string list Util.String.Map.t ref = ref Util.String.Map.empty class type ['a] repr = object @@ -121,6 +122,18 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] + +let line_end_of_string = function +| "unix" -> `UNIX +| "windows" -> `WINDOWS +| _ -> `DEFAULT + +let line_end_to_string = function +| `UNIX -> "unix" +| `WINDOWS -> "windows" +| `DEFAULT -> "default" + let use_default_doc_url = "(automatic)" module Repr = @@ -381,6 +394,10 @@ let stop_before = let reset_on_tab_switch = new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool) +let line_ending = + let repr = Repr.custom line_end_to_string line_end_of_string in + new preference ~name:["line_ending"] ~init:`DEFAULT ~repr + let vertical_tabs = new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool) @@ -451,7 +468,7 @@ let create_tag name default = let iter table = let tag = GText.tag ~name () in table#add tag#as_tag; - pref#connect#changed (fun _ -> set_tag tag); + ignore (pref#connect#changed (fun _ -> set_tag tag)); set_tag tag; in List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; @@ -601,19 +618,19 @@ let save_pref () = then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in let add = Util.String.Map.add in - let (++) x f = f x in let fold key obj accu = add key (obj.get ()) accu in - - (Util.String.Map.fold fold !preferences Util.String.Map.empty) ++ - Config_lexer.print_file pref_file + let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in + let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in + Config_lexer.print_file pref_file prefs let load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let m = Config_lexer.load_file loaded_pref_file in let iter name v = - try (Util.String.Map.find name !preferences).set v - with _ -> () + if Util.String.Map.mem name !preferences then + try (Util.String.Map.find name !preferences).set v with _ -> () + else unknown_preferences := Util.String.Map.add name v !unknown_preferences in Util.String.Map.iter iter m @@ -818,6 +835,15 @@ let configure ?(apply=(fun () -> ())) () = (string_of_inputenc encoding#get) in + let line_ending = + combo + "EOL character" + ~f:(fun s -> line_ending#set (line_end_of_string s)) + ~new_allowed:false + ["unix"; "windows"; "default"] + (line_end_to_string line_ending#get) + in + let source_style = combo "Highlighting style:" ~f:source_style#set ~new_allowed:false @@ -892,7 +918,7 @@ let configure ?(apply=(fun () -> ())) () = in let doc_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";""]); + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["refman";"html"]); Coq_config.wwwrefman; use_default_doc_url ] in @@ -905,7 +931,7 @@ let configure ?(apply=(fun () -> ())) () = doc_url#get in let library_url = let predefined = [ - "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]); + "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["stdlib";"html"]); Coq_config.wwwstdlib ] in combo @@ -973,7 +999,7 @@ let configure ?(apply=(fun () -> ())) () = Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings; + encodings; line_ending; ]); Section("Project", Some (`STOCK "gtk-page-setup"), [project_file_name;read_project; diff --git a/ide/preferences.mli b/ide/preferences.mli index 426b0a328e..801869d1dc 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -11,6 +11,7 @@ val style_manager : GSourceView2.source_style_scheme_manager type project_behavior = Ignore_args | Append_args | Subst_args type inputenc = Elocale | Eutf8 | Emanual of string +type line_ending = [ `DEFAULT | `WINDOWS | `UNIX ] type tag = { tag_fg_color : string option; @@ -79,6 +80,7 @@ val window_height : int preference val auto_complete : bool preference val stop_before : bool preference val reset_on_tab_switch : bool preference +val line_ending : line_ending preference val vertical_tabs : bool preference val opposite_tabs : bool preference val background_color : string preference diff --git a/ide/sentence.ml b/ide/sentence.ml index 6897779e80..e332682dd0 100644 --- a/ide/sentence.ml +++ b/ide/sentence.ml @@ -16,6 +16,7 @@ let split_slice_lax (buffer:GText.buffer) start stop = buffer#remove_tag ~start ~stop Tags.Script.sentence; buffer#remove_tag ~start ~stop Tags.Script.error; + buffer#remove_tag ~start ~stop Tags.Script.warning; buffer#remove_tag ~start ~stop Tags.Script.error_bg; let slice = buffer#get_text ~start ~stop () in let apply_tag off tag = diff --git a/ide/session.ml b/ide/session.ml index cdec392ecc..fc6340d283 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -108,10 +108,10 @@ let set_buffer_handlers let id = ref 0 in fun () -> incr id; !id in let running_action = ref None in - let cancel_signal reason = + let cancel_signal ?(stop_emit=true) reason = Minilib.log ("user_action cancelled: "^reason); action_was_cancelled := true; - GtkSignal.stop_emit () in + if stop_emit then GtkSignal.stop_emit () in let del_mark () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in @@ -124,7 +124,7 @@ let set_buffer_handlers fun () -> (* If Coq is busy due to the current action, we don't cancel *) match !running_action with | Some aid when aid = action -> () - | _ -> cancel_signal "Coq busy" in + | _ -> cancel_signal ~stop_emit:false "Coq busy" in Coq.try_grab coqtop action fallback in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in @@ -195,12 +195,8 @@ let set_buffer_handlers to a point indicated by coq. *) if !no_coq_action_required then begin let start, stop = get_start (), get_stop () in - buffer#remove_tag Tags.Script.error ~start ~stop; - buffer#remove_tag Tags.Script.error_bg ~start ~stop; - buffer#remove_tag Tags.Script.tooltip ~start ~stop; - buffer#remove_tag Tags.Script.processed ~start ~stop; - buffer#remove_tag Tags.Script.to_process ~start ~stop; - buffer#remove_tag Tags.Script.incomplete ~start ~stop; + List.iter (fun tag -> buffer#remove_tag tag ~start ~stop) + Tags.Script.ephemere; Sentence.tag_on_insert buffer end; end in diff --git a/ide/tags.ml b/ide/tags.ml index 9ccff9fb51..e4510e7af4 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -18,6 +18,7 @@ struct let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] + let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"] let error_bg = make_tag table ~name:"error_bg" [] let to_process = make_tag table ~name:"to_process" [] let processed = make_tag table ~name:"processed" [] @@ -29,9 +30,11 @@ struct let sentence = make_tag table ~name:"sentence" [] let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *) + let ephemere = + [error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified] + let all = - [comment; error; error_bg; to_process; processed; incomplete; unjustified; - found; sentence; tooltip] + comment :: found :: sentence :: ephemere let edit_zone = let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in diff --git a/ide/tags.mli b/ide/tags.mli index 5a932f3300..02e15a5ae4 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -11,6 +11,7 @@ sig val table : GText.tag_table val comment : GText.tag val error : GText.tag + val warning : GText.tag val error_bg : GText.tag val to_process : GText.tag val processed : GText.tag @@ -20,6 +21,7 @@ sig val sentence : GText.tag val tooltip : GText.tag val edit_zone : GText.tag (* for debugging *) + val ephemere : GText.tag list val all : GText.tag list end diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index f445f2e08d..680da7f54b 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -189,7 +189,8 @@ match sm with end | SetEntryType (s, _) -> ["entrytype", s] | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in ["format-"^system, s; "begin", start; "end", stop] @@ -238,6 +239,8 @@ and pp_local_binder lb = (* don't know what it is for now *) let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in xmlTyped (ppl @ [pp_expr ce]) + | LocalPattern _ -> + assert false and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with | AssumExpr (_, ce) -> pp_expr ce @@ -351,6 +354,7 @@ and pp_cases_pattern_expr cpe = xmlApply loc (xmlOperator "delimiter" ~attr:["name", delim] loc :: [pp_cases_pattern_expr cpe]) + | CPatCast _ -> assert false and pp_case_expr (e, name, pat) = match name, pat with | None, None -> xmlScrutinee [pp_expr e] @@ -705,6 +709,7 @@ let rec tmpp v loc = | VernacSetStrategy _ as x -> xmlTODO loc x | VernacUnsetOption _ as x -> xmlTODO loc x | VernacSetOption _ as x -> xmlTODO loc x + | VernacSetAppendOption _ as x -> xmlTODO loc x | VernacAddOption _ as x -> xmlTODO loc x | VernacRemoveOption _ as x -> xmlTODO loc x | VernacMemOption _ as x -> xmlTODO loc x diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 758f383d6d..0330b8eff1 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -43,6 +43,7 @@ let message_view () : message_view = ~tag_table:Tags.Message.table () in let text_buffer = new GText.buffer buffer#as_buffer in + let mark = buffer#create_mark ~left_gravity:false buffer#start_iter in let box = GPack.vbox () in let scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:(box#pack ~expand:true) () in @@ -69,7 +70,8 @@ let message_view () : message_view = new message_view_signals_impl box#as_widget push method clear = - buffer#set_text "" + buffer#set_text ""; + buffer#move_mark (`MARK mark) ~where:buffer#start_iter method push level msg = let tags = match level with @@ -83,8 +85,9 @@ let message_view () : message_view = | Xml_datatype.Element (_, _, children) -> List.exists non_empty children in if non_empty (Richpp.repr msg) then begin - Ideutils.insert_xml buffer ~tags msg; - buffer#insert (*~tags*) "\n"; + let mark = `MARK mark in + Ideutils.insert_xml ~mark buffer ~tags msg; + buffer#insert ~iter:(buffer#get_iter_at_mark mark) "\n"; push#call (level, msg) end diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml index e7e4d0cebc..40ab4ce9cb 100644 --- a/ide/xml_printer.ml +++ b/ide/xml_printer.ml @@ -17,65 +17,65 @@ type t = target let make x = x let buffer_pcdata tmp text = - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in let l = String.length text in for p = 0 to l-1 do match text.[p] with - | ' ' -> output " "; - | '>' -> output ">" - | '<' -> output "<" + | ' ' -> puts " "; + | '>' -> puts ">" + | '<' -> puts "<" | '&' -> if p < l - 1 && text.[p + 1] = '#' then - output' '&' + putc '&' else - output "&" - | '\'' -> output "'" - | '"' -> output """ - | c -> output' c + puts "&" + | '\'' -> puts "'" + | '"' -> puts """ + | c -> putc c done let buffer_attr tmp (n,v) = - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in - output' ' '; - output n; - output "=\""; + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in + putc ' '; + puts n; + puts "=\""; let l = String.length v in for p = 0 to l - 1 do match v.[p] with - | '\\' -> output "\\\\" - | '"' -> output "\\\"" - | '<' -> output "<" - | '&' -> output "&" - | c -> output' c + | '\\' -> puts "\\\\" + | '"' -> puts "\\\"" + | '<' -> puts "<" + | '&' -> puts "&" + | c -> putc c done; - output' '"' + putc '"' let to_buffer tmp x = let pcdata = ref false in - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in let rec loop = function | Element (tag,alist,[]) -> - output' '<'; - output tag; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output "/>"; + puts "/>"; pcdata := false; | Element (tag,alist,l) -> - output' '<'; - output tag; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output' '>'; + putc '>'; pcdata := false; List.iter loop l; - output "</"; - output tag; - output' '>'; + puts "</"; + puts tag; + putc '>'; pcdata := false; | PCData text -> - if !pcdata then output' ' '; + if !pcdata then putc ' '; buffer_pcdata tmp text; pcdata := true; in @@ -93,42 +93,42 @@ let to_string x = let to_string_fmt x = let tmp = Buffer.create 200 in - let output = Buffer.add_string tmp in - let output' = Buffer.add_char tmp in + let puts = Buffer.add_string tmp in + let putc = Buffer.add_char tmp in let rec loop ?(newl=false) tab = function | Element (tag, alist, []) -> - output tab; - output' '<'; - output tag; + puts tab; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output "/>"; - if newl then output' '\n'; + puts "/>"; + if newl then putc '\n'; | Element (tag, alist, [PCData text]) -> - output tab; - output' '<'; - output tag; + puts tab; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output ">"; + puts ">"; buffer_pcdata tmp text; - output "</"; - output tag; - output' '>'; - if newl then output' '\n'; + puts "</"; + puts tag; + putc '>'; + if newl then putc '\n'; | Element (tag, alist, l) -> - output tab; - output' '<'; - output tag; + puts tab; + putc '<'; + puts tag; List.iter (buffer_attr tmp) alist; - output ">\n"; + puts ">\n"; List.iter (loop ~newl:true (tab^" ")) l; - output tab; - output "</"; - output tag; - output' '>'; - if newl then output' '\n'; + puts tab; + puts "</"; + puts tag; + putc '>'; + if newl then putc '\n'; | PCData text -> buffer_pcdata tmp text; - if newl then output' '\n'; + if newl then putc '\n'; in loop "" x; Buffer.contents tmp diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index a55d19aa1b..aecb317bcb 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -607,7 +607,7 @@ let abstract_eval_call : type a. _ -> a call -> a value = fun handler c -> | PrintAst x -> mkGood (handler.print_ast x) | Annotate x -> mkGood (handler.annotate x) with any -> - let any = Errors.push any in + let any = CErrors.push any in Fail (handler.handle_exn any) (** brain dead code, edit if protocol messages are added/removed *) @@ -769,34 +769,37 @@ let document to_string_fmt = open Feedback let of_message_level = function - | Debug s -> - Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s] + | Debug -> + Serialize.constructor "message_level" "debug" [] | Info -> Serialize.constructor "message_level" "info" [] | Notice -> Serialize.constructor "message_level" "notice" [] | Warning -> Serialize.constructor "message_level" "warning" [] | Error -> Serialize.constructor "message_level" "error" [] let to_message_level = Serialize.do_match "message_level" (fun s args -> match s with - | "debug" -> Debug (Serialize.raw_string args) + | "debug" -> Debug | "info" -> Info | "notice" -> Notice | "warning" -> Warning | "error" -> Error | x -> raise Serialize.(Marshal_error("error level",PCData x))) -let of_message lvl msg = +let of_message lvl loc msg = let lvl = of_message_level lvl in + let xloc = of_option of_loc loc in let content = of_richpp msg in - Xml_datatype.Element ("message", [], [lvl; content]) + Xml_datatype.Element ("message", [], [lvl; xloc; content]) + let to_message xml = match xml with - | Xml_datatype.Element ("message", [], [lvl; content]) -> - Message(to_message_level lvl, to_richpp content) + | Xml_datatype.Element ("message", [], [lvl; xloc; content]) -> + Message(to_message_level lvl, to_option to_loc xloc, to_richpp content) | x -> raise (Marshal_error("message",x)) -let is_message = function - | Xml_datatype.Element ("message", [], [lvl; content]) -> - Some (to_message_level lvl, to_richpp content) - | _ -> None +let is_message xml = + try begin match to_message xml with + | Message(l,c,m) -> Some (l,c,m) + | _ -> None + end with | Marshal_error _ -> None let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with | "addedaxiom", _ -> AddedAxiom @@ -809,7 +812,6 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with to_string modpath, to_string ident, to_string ty) | "globdef", [loc; ident; secpath; ty] -> GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) - | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) | "inprogress", [n] -> InProgress (to_int n) | "workerstatus", [ns] -> let n, s = to_pair to_string to_string ns in @@ -843,8 +845,6 @@ let of_feedback_content = function of_string ident; of_string secpath; of_string ty ] - | ErrorMsg(loc, s) -> - constructor "feedback_content" "errormsg" [of_loc loc; of_string s] | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] | WorkerStatus(n,s) -> constructor "feedback_content" "workerstatus" @@ -861,7 +861,7 @@ let of_feedback_content = function constructor "feedback_content" "fileloaded" [ of_string dirpath; of_string filename ] - | Message (l,m) -> constructor "feedback_content" "message" [ of_message l m ] + | Message (l,loc,m) -> constructor "feedback_content" "message" [ of_message l loc m ] let of_edit_or_state_id = function | Edit id -> ["object","edit"], of_edit_id id diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli index 6bca8772ed..1bb9989704 100644 --- a/ide/xmlprotocol.mli +++ b/ide/xmlprotocol.mli @@ -66,7 +66,7 @@ val of_feedback : Feedback.feedback -> xml val to_feedback : xml -> Feedback.feedback val is_feedback : xml -> bool -val is_message : xml -> (Feedback.level * Richpp.richpp) option -val of_message : Feedback.level -> Richpp.richpp -> xml +val is_message : xml -> (Feedback.level * Loc.t option * Richpp.richpp) option +val of_message : Feedback.level -> Loc.t option -> Richpp.richpp -> xml (* val to_message : xml -> Feedback.message *) |