diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/coq.ml | 16 | ||||
-rw-r--r-- | ide/coqOps.ml | 37 | ||||
-rw-r--r-- | ide/coqide.ml | 257 | ||||
-rw-r--r-- | ide/fileOps.ml | 8 | ||||
-rw-r--r-- | ide/ide.mllib | 2 | ||||
-rw-r--r-- | ide/ide_slave.ml | 21 | ||||
-rw-r--r-- | ide/ideutils.ml | 51 | ||||
-rw-r--r-- | ide/ideutils.mli | 9 | ||||
-rw-r--r-- | ide/interface.mli | 9 | ||||
-rw-r--r-- | ide/nanoPG.ml | 2 | ||||
-rw-r--r-- | ide/preferences.ml | 1201 | ||||
-rw-r--r-- | ide/preferences.mli | 169 | ||||
-rw-r--r-- | ide/session.ml | 22 | ||||
-rw-r--r-- | ide/session.mli | 1 | ||||
-rw-r--r-- | ide/tags.ml | 54 | ||||
-rw-r--r-- | ide/tags.mli | 19 | ||||
-rw-r--r-- | ide/wg_Command.ml | 25 | ||||
-rw-r--r-- | ide/wg_Command.mli | 2 | ||||
-rw-r--r-- | ide/wg_Completion.ml | 2 | ||||
-rw-r--r-- | ide/wg_MessageView.ml | 39 | ||||
-rw-r--r-- | ide/wg_MessageView.mli | 11 | ||||
-rw-r--r-- | ide/wg_ProofView.ml | 34 | ||||
-rw-r--r-- | ide/wg_ScriptView.ml | 29 | ||||
-rw-r--r-- | ide/wg_Segment.ml | 3 | ||||
-rw-r--r-- | ide/xmlprotocol.ml | 28 |
25 files changed, 1028 insertions, 1023 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index b7753e6e8..a60f327b4 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -125,7 +125,7 @@ and asks_for_coqtop args = ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in match pb_mes#run () with | `YES -> - let () = current.cmd_coqtop <- None in + let () = cmd_coqtop#set None in let () = custom_coqtop := None in let () = pb_mes#destroy () in filter_coq_opts args @@ -302,13 +302,13 @@ let handle_intermediate_message handle xml = let logger = match handle.waiting_for with | Some (_, l) -> l | None -> function - | Pp.Error -> Minilib.log ~level:`ERROR - | Pp.Info -> Minilib.log ~level:`INFO - | Pp.Notice -> Minilib.log ~level:`NOTICE - | Pp.Warning -> Minilib.log ~level:`WARNING - | Pp.Debug _ -> Minilib.log ~level:`DEBUG + | Pp.Error -> fun s -> Minilib.log ~level:`ERROR (xml_to_string s) + | Pp.Info -> fun s -> Minilib.log ~level:`INFO (xml_to_string s) + | Pp.Notice -> fun s -> Minilib.log ~level:`NOTICE (xml_to_string s) + | Pp.Warning -> fun s -> Minilib.log ~level:`WARNING (xml_to_string s) + | Pp.Debug _ -> fun s -> Minilib.log ~level:`DEBUG (xml_to_string s) in - logger level content + logger level (Richpp.richpp_of_xml content) let handle_feedback feedback_processor xml = let feedback = Feedback.to_feedback xml in @@ -336,7 +336,7 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let lex = Lexing.from_string s in let p = Xml_parser.make (Xml_parser.SLexbuf lex) in let rec loop () = - let xml = Xml_parser.parse p in + let xml = Xml_parser.parse ~do_not_canonicalize:true p in let l_end = Lexing.lexeme_end lex in state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; diff --git a/ide/coqOps.ml b/ide/coqOps.ml index ba9ab9672..8bfc70b63 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -130,8 +130,6 @@ end = struct end open SentenceId -let prefs = Preferences.current - let log msg : unit task = Coq.lift (fun () -> Minilib.log msg) @@ -160,12 +158,19 @@ object end let flags_to_color f = - let of_col c = `NAME (Tags.string_of_color c) in if List.mem `PROCESSING f then `NAME "blue" else if List.mem `ERROR f then `NAME "red" else if List.mem `UNSAFE f then `NAME "orange" else if List.mem `INCOMPLETE f then `NAME "gray" - else of_col (Tags.get_processed_color ()) + else `NAME Preferences.processed_color#get + +let validate s = + let open Xml_datatype in + let rec validate = function + | PCData s -> Glib.Utf8.validate s + | Element (_, _, children) -> List.for_all validate children + in + validate (Richpp.repr s) module Doc = Document @@ -322,7 +327,7 @@ object(self) method raw_coq_query phrase = let action = log "raw_coq_query starting now" in let display_error s = - if not (Glib.Utf8.validate s) then + if not (validate s) then flash_info "This error is so nasty that I can't even display it." else messages#add s; in @@ -331,7 +336,7 @@ object(self) let next = function | Fail (_, _, err) -> display_error err; Coq.return () | Good msg -> - messages#add msg; Coq.return () + messages#add_string msg; Coq.return () in Coq.bind (Coq.seq action query) next @@ -559,7 +564,7 @@ object(self) if Queue.is_empty queue then conclude topstack else match Queue.pop queue, topstack with | `Skip(start,stop), [] -> - logger Pp.Error "You muse close the proof with Qed or Admitted"; + logger Pp.Error (Richpp.richpp_of_string "You muse close the proof with Qed or Admitted"); self#discard_command_queue queue; conclude [] | `Skip(start,stop), (_,s) :: topstack -> @@ -575,7 +580,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Pp.Notice msg; + logger Pp.Notice (Richpp.richpp_of_string msg); self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -583,7 +588,7 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Pp.Notice msg; + logger Pp.Notice (Richpp.richpp_of_string msg); self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) @@ -602,7 +607,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Pp.Info "All proof terms checked by the kernel"; + messages#push Pp.Info (Richpp.richpp_of_string "All proof terms checked by the kernel"); Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status ~logger:messages#push true) next @@ -630,7 +635,7 @@ object(self) method private process_until_iter iter = let until _ start stop = - if prefs.Preferences.stop_before then stop#compare iter > 0 + if Preferences.stop_before#get then stop#compare iter > 0 else start#compare iter >= 0 in self#process_until until false @@ -696,7 +701,7 @@ object(self) self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> - if loc <> None then messages#push Pp.Error "Fixme LOC"; + if loc <> None then messages#push Pp.Error (Richpp.richpp_of_string "Fixme LOC"); messages#push Pp.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id @@ -772,7 +777,7 @@ object(self) self#show_goals in let display_error (loc, s) = - if not (Glib.Utf8.validate s) then + if not (validate s) then flash_info "This error is so nasty that I can't even display it." else messages#add s in @@ -782,10 +787,10 @@ object(self) let next = function | Fail (_, l, str) -> (* FIXME: check *) display_error (l, str); - messages#add ("Unsuccessfully tried: "^phrase); + messages#add (Richpp.richpp_of_string ("Unsuccessfully tried: "^phrase)); more | Good msg -> - messages#add msg; + messages#add_string msg; stop Tags.Script.processed in Coq.bind (Coq.seq action query) next @@ -829,7 +834,7 @@ object(self) method initialize = let get_initial_state = let next = function - | Fail _ -> messages#set ("Couln't initialize Coq"); Coq.return () + | Fail _ -> messages#set (Richpp.richpp_of_string "Couln't initialize Coq"); Coq.return () | Good id -> initial_state <- id; Coq.return () in Coq.bind (Coq.init (get_filename ())) next in Coq.seq get_initial_state Coq.PrintOpt.enforce diff --git a/ide/coqide.ml b/ide/coqide.ml index c0e228125..e591f205f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -44,8 +44,6 @@ open Session (** {2 Some static elements } *) -let prefs = Preferences.current - (** The arguments that will be passed to coqtop. No quoting here, since no /bin/sh when using create_process instead of open_process. *) let custom_project_files = ref [] @@ -87,9 +85,9 @@ let make_coqtop_args = function |None -> "", !sup_args |Some the_file -> let get_args f = Project_file.args_from_project f - !custom_project_files prefs.project_file_name + !custom_project_files project_file_name#get in - match prefs.read_project with + match read_project#get with |Ignore_args -> "", !sup_args |Append_args -> let fname, args = get_args the_file in fname, args @ !sup_args @@ -164,7 +162,6 @@ let load_file ?(maycreate=false) f = input_buffer#place_cursor ~where:input_buffer#start_iter; Sentence.tag_all input_buffer; session.script#clear_undo (); - !refresh_editor_hook (); Minilib.log "Loading: success"; end with e -> flash_info ("Load failed: "^(Printexc.to_string e)) @@ -250,7 +247,6 @@ module File = struct let newfile _ = let session = create_session None in let index = notebook#append_term session in - !refresh_editor_hook (); notebook#goto_page index let load _ = @@ -319,13 +315,13 @@ let export kind sn = | _ -> assert false in let cmd = - local_cd f ^ prefs.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ + local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1" in - sn.messages#set ("Running: "^cmd); + sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); let finally st = flash_info (cmd ^ pr_exit_status st) in - run_command sn.messages#add finally cmd + run_command (fun msg -> sn.messages#add_string msg) finally cmd let export kind = cb_on_current_term (export kind) @@ -334,8 +330,8 @@ let print sn = |None -> flash_info "Cannot print: this buffer has no name" |Some f_name -> let cmd = - local_cd f_name ^ prefs.cmd_coqdoc ^ " -ps " ^ - Filename.quote (Filename.basename f_name) ^ " | " ^ prefs.cmd_print + local_cd f_name ^ cmd_coqdoc#get ^ " -ps " ^ + Filename.quote (Filename.basename f_name) ^ " | " ^ cmd_print#get in let w = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () @@ -378,17 +374,17 @@ end let reset_revert_timer () = FileOps.revert_timer.kill (); - if prefs.global_auto_revert then + if global_auto_revert#get then FileOps.revert_timer.run - ~ms:prefs.global_auto_revert_delay + ~ms:global_auto_revert_delay#get ~callback:(fun () -> File.revert_all (); true) let reset_autosave_timer () = let autosave sn = try sn.fileops#auto_save with _ -> () in let autosave_all () = List.iter autosave notebook#pages; true in FileOps.autosave_timer.kill (); - if prefs.auto_save then - FileOps.autosave_timer.run ~ms:prefs.auto_save_delay ~callback:autosave_all + if auto_save#get then + FileOps.autosave_timer.run ~ms:auto_save_delay#get ~callback:autosave_all (** Export of functions used in [coqide_main] : *) @@ -408,8 +404,8 @@ let coq_makefile sn = match sn.fileops#filename with |None -> flash_info "Cannot make makefile: this buffer has no name" |Some f -> - let cmd = local_cd f ^ prefs.cmd_coqmakefile in - let finally st = flash_info (current.cmd_coqmakefile ^ pr_exit_status st) + let cmd = local_cd f ^ cmd_coqmakefile#get in + let finally st = flash_info (cmd_coqmakefile#get ^ pr_exit_status st) in run_command ignore finally cmd @@ -421,7 +417,7 @@ let editor sn = |Some f -> File.save (); let f = Filename.quote f in - let cmd = Util.subst_command_placeholder prefs.cmd_editor f in + let cmd = Util.subst_command_placeholder cmd_editor#get f in run_command ignore (fun _ -> sn.fileops#revert) cmd let editor = cb_on_current_term editor @@ -431,13 +427,13 @@ let compile sn = match sn.fileops#filename with |None -> flash_info "Active buffer has no name" |Some f -> - let cmd = prefs.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f)) + let cmd = cmd_coqc#get ^ " -I " ^ (Filename.quote (Filename.dirname f)) ^ " " ^ (Filename.quote f) ^ " 2>&1" in let buf = Buffer.create 1024 in - sn.messages#set ("Running: "^cmd); + sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd)); let display s = - sn.messages#add s; + sn.messages#add_string s; Buffer.add_string buf s in let finally st = @@ -445,8 +441,8 @@ let compile sn = flash_info (f ^ " successfully compiled") else begin flash_info (f ^ " failed to compile"); - sn.messages#set "Compilation output:\n"; - sn.messages#add (Buffer.contents buf); + sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); + sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf)); end in run_command display finally cmd @@ -467,17 +463,17 @@ let make sn = |None -> flash_info "Cannot make: this buffer has no name" |Some f -> File.saveall (); - let cmd = local_cd f ^ prefs.cmd_make ^ " 2>&1" in - sn.messages#set "Compilation output:\n"; + let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in + sn.messages#set (Richpp.richpp_of_string "Compilation output:\n"); Buffer.reset last_make_buf; last_make := ""; last_make_index := 0; last_make_dir := Filename.dirname f; let display s = - sn.messages#add s; + sn.messages#add_string s; Buffer.add_string last_make_buf s in - let finally st = flash_info (current.cmd_make ^ pr_exit_status st) + let finally st = flash_info (cmd_make#get ^ pr_exit_status st) in run_command display finally cmd @@ -512,11 +508,11 @@ let next_error sn = let stopi = b#get_iter_at_byte ~line:(line-1) stop in b#apply_tag Tags.Script.error ~start:starti ~stop:stopi; b#place_cursor ~where:starti; - sn.messages#set error_msg; + sn.messages#set (Richpp.richpp_of_string error_msg); sn.script#misc#grab_focus () with Not_found -> last_make_index := 0; - sn.messages#set "No more errors.\n" + sn.messages#set (Richpp.richpp_of_string "No more errors.\n") let next_error = cb_on_current_term next_error @@ -537,7 +533,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready"^ (if current.nanoPG then ", [μPG]" else "") ^ path ^ name); + display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name); Coq.return () in Coq.bind (Coq.status ~logger:sn.messages#push false) next @@ -722,7 +718,7 @@ let initial_about () = else "" in let msg = initial_string ^ version_info ^ log_file_message () in - on_current_term (fun term -> term.messages#add msg) + on_current_term (fun term -> term.messages#add_string msg) let coq_icon () = (* May raise Nof_found *) @@ -787,7 +783,7 @@ let coqtop_arguments sn = let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in let () = sn.messages#clear in - sn.messages#push Pp.Error msg + sn.messages#push Pp.Error (Richpp.richpp_of_string msg) else dialog#destroy () in let _ = entry#connect#activate ok_cb in @@ -809,69 +805,19 @@ let zoom_fit sn = let cols = script#right_margin_position in let pango_ctx = script#misc#pango_context in let layout = pango_ctx#create_layout in - let fsize = Pango.Font.get_size current.text_font in + let fsize = Pango.Font.get_size (Pango.Font.from_string text_font#get) in Pango.Layout.set_text layout (String.make cols 'X'); let tlen = fst (Pango.Layout.get_pixel_size layout) in - Pango.Font.set_size current.text_font + Pango.Font.set_size (Pango.Font.from_string text_font#get) (fsize * space / tlen / Pango.scale * Pango.scale); - save_pref (); - !refresh_editor_hook () + save_pref () end (** Refresh functions *) -let refresh_editor_prefs () = - let wrap_mode = if prefs.dynamic_word_wrap then `WORD else `NONE in - let show_spaces = - if prefs.show_spaces then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *) - else 0 - in - let fd = prefs.text_font in - let clr = Tags.color_of_string prefs.background_color - in - let iter_session sn = - (* Editor settings *) - sn.script#set_wrap_mode wrap_mode; - sn.script#set_show_line_numbers prefs.show_line_number; - sn.script#set_auto_indent prefs.auto_indent; - sn.script#set_highlight_current_line prefs.highlight_current_line; - - (* Hack to handle missing binding in lablgtk *) - let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int } - in - Gobject.set conv sn.script#as_widget show_spaces; - - sn.script#set_show_right_margin prefs.show_right_margin; - if prefs.show_progress_bar then sn.segment#misc#show () else sn.segment#misc#hide (); - sn.script#set_insert_spaces_instead_of_tabs - prefs.spaces_instead_of_tabs; - sn.script#set_tab_width prefs.tab_length; - sn.script#set_auto_complete prefs.auto_complete; - - (* Fonts *) - sn.script#misc#modify_font fd; - sn.proof#misc#modify_font fd; - sn.messages#modify_font fd; - sn.command#refresh_font (); - - (* Colors *) - Tags.set_processing_color (Tags.color_of_string current.processing_color); - Tags.set_processed_color (Tags.color_of_string current.processed_color); - Tags.set_error_color (Tags.color_of_string current.error_color); - Tags.set_error_fg_color (Tags.color_of_string current.error_fg_color); - sn.script#misc#modify_base [`NORMAL, `COLOR clr]; - sn.proof#misc#modify_base [`NORMAL, `COLOR clr]; - sn.messages#refresh_color (); - sn.command#refresh_color (); - sn.errpage#refresh_color (); - sn.jobpage#refresh_color (); - - in - List.iter iter_session notebook#pages - let refresh_notebook_pos () = - let pos = match prefs.vertical_tabs, prefs.opposite_tabs with + let pos = match vertical_tabs#get, opposite_tabs#get with | false, false -> `TOP | false, true -> `BOTTOM | true , false -> `LEFT @@ -906,7 +852,7 @@ let toggle_items menu_name l = let f d = let label = d.Opt.label in let k, name = get_shortcut label in - let accel = Option.map ((^) prefs.modifier_for_display) k in + let accel = Option.map ((^) modifier_for_display#get) k in toggle_item name ~label ?accel ~active:d.Opt.init ~callback:(printopts_callback d.Opt.opts) menu_name @@ -948,7 +894,7 @@ let alpha_items menu_name item_name l = Caveat: the offset is now from the start of the text. *) let template_item (text, offset, len, key) = - let modifier = prefs.modifier_for_templates in + let modifier = modifier_for_templates#get in let idx = String.index text ' ' in let name = String.sub text 0 idx in let label = "_"^name^" __" in @@ -976,7 +922,7 @@ let build_ui () = let w = GWindow.window ~wm_class:"CoqIde" ~wm_name:"CoqIde" ~allow_grow:true ~allow_shrink:true - ~width:prefs.window_width ~height:prefs.window_height + ~width:window_width#get ~height:window_height#get ~title:"CoqIde" () in let () = @@ -1074,77 +1020,60 @@ let build_ui () = ~callback:(fun _ -> notebook#next_page ()); item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus") ~stock:`ZOOM_IN ~callback:(fun _ -> - Pango.Font.set_size current.text_font - (Pango.Font.get_size current.text_font + Pango.scale); - save_pref (); - !refresh_editor_hook ()); + let ft = Pango.Font.from_string text_font#get in + Pango.Font.set_size ft (Pango.Font.get_size ft + Pango.scale); + text_font#set (Pango.Font.to_string ft); + save_pref ()); item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus") ~stock:`ZOOM_OUT ~callback:(fun _ -> - Pango.Font.set_size current.text_font - (Pango.Font.get_size current.text_font - Pango.scale); - save_pref (); - !refresh_editor_hook ()); + let ft = Pango.Font.from_string text_font#get in + Pango.Font.set_size ft (Pango.Font.get_size ft - Pango.scale); + text_font#set (Pango.Font.to_string ft); + save_pref ()); item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0") ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit); toggle_item "Show Toolbar" ~label:"Show _Toolbar" - ~active:(prefs.show_toolbar) - ~callback:(fun _ -> - prefs.show_toolbar <- not prefs.show_toolbar; - !refresh_toolbar_hook ()); + ~active:(show_toolbar#get) + ~callback:(fun _ -> show_toolbar#set (not show_toolbar#get)); item "Query Pane" ~label:"_Query Pane" ~accel:"F1" ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane) ]; toggle_items view_menu Coq.PrintOpt.bool_items; - menu navigation_menu [ - item "Navigation" ~label:"_Navigation"; - item "Forward" ~label:"_Forward" ~stock:`GO_DOWN ~callback:Nav.forward_one - ~tooltip:"Forward one command" - ~accel:(prefs.modifier_for_navigation^"Down"); - item "Backward" ~label:"_Backward" ~stock:`GO_UP ~callback:Nav.backward_one - ~tooltip:"Backward one command" - ~accel:(prefs.modifier_for_navigation^"Up"); - item "Go to" ~label:"_Go to" ~stock:`JUMP_TO ~callback:Nav.goto - ~tooltip:"Go to cursor" - ~accel:(prefs.modifier_for_navigation^"Right"); - item "Start" ~label:"_Start" ~stock:`GOTO_TOP ~callback:Nav.restart - ~tooltip:"Restart coq" - ~accel:(prefs.modifier_for_navigation^"Home"); - item "End" ~label:"_End" ~stock:`GOTO_BOTTOM ~callback:Nav.goto_end - ~tooltip:"Go to end" - ~accel:(prefs.modifier_for_navigation^"End"); - item "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:Nav.interrupt - ~tooltip:"Interrupt computations" - ~accel:(prefs.modifier_for_navigation^"Break"); -(* wait for this available in GtkSourceView ! - item "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE - ~callback:(fun _ -> let sess = notebook#current_term in - toggle_proof_visibility sess.buffer - sess.analyzed_view#get_insert) ~tooltip:"Hide proof" - ~accel:(prefs.modifier_for_navigation^"h");*) - item "Previous" ~label:"_Previous" ~stock:`GO_BACK - ~callback:Nav.previous_occ - ~tooltip:"Previous occurence" - ~accel:(prefs.modifier_for_navigation^"less"); - item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ - ~tooltip:"Next occurence" - ~accel:(prefs.modifier_for_navigation^"greater"); - item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document - ~tooltip:"Fully check the document" - ~accel:(current.modifier_for_navigation^"f"); - ]; + let navitem (text, label, stock, callback, tooltip, accel) = + let accel = modifier_for_navigation#get ^ accel in + item text ~label ~stock ~callback ~tooltip ~accel + in + menu navigation_menu begin + [ + (fun e -> item "Navigation" ~label:"_Navigation" e); + ] @ List.map navitem [ + ("Forward", "_Forward", `GO_DOWN, Nav.forward_one, "Forward one command", "Down"); + ("Backward", "_Backward", `GO_UP, Nav.backward_one, "Backward one command", "Up"); + ("Go to", "_Go to", `JUMP_TO, Nav.goto, "Go to cursor", "Right"); + ("Start", "_Start", `GOTO_TOP, Nav.restart, "Restart coq", "Home"); + ("End", "_End", `GOTO_BOTTOM, Nav.goto_end, "Go to end", "End"); + ("Interrupt", "_Interrupt", `STOP, Nav.interrupt, "Interrupt computations", "Break"); + (* wait for this available in GtkSourceView ! + ("Hide", "_Hide", `MISSING_IMAGE, + ~callback:(fun _ -> let sess = notebook#current_term in + toggle_proof_visibility sess.buffer sess.analyzed_view#get_insert), "Hide proof", "h"); *) + ("Previous", "_Previous", `GO_BACK, Nav.previous_occ, "Previous occurence", "less"); + ("Next", "_Next", `GO_FORWARD, Nav.next_occ, "Next occurence", "greater"); + ("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f"); + ] end; let tacitem s sc = item s ~label:("_"^s) - ~accel:(prefs.modifier_for_tactics^sc) + ~accel:(modifier_for_tactics#get^sc) ~callback:(tactic_wizard_callback [s]) in menu tactics_menu [ item "Try Tactics" ~label:"_Try Tactics"; item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO - ~tooltip:"Proof Wizard" ~accel:(prefs.modifier_for_tactics^"dollar") - ~callback:(tactic_wizard_callback prefs.automatic_tactics); + ~tooltip:"Proof Wizard" ~accel:(modifier_for_tactics#get^"dollar") + ~callback:(tactic_wizard_callback automatic_tactics#get); tacitem "auto" "a"; tacitem "auto with *" "asterisk"; tacitem "eauto" "e"; @@ -1166,7 +1095,7 @@ let build_ui () = template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F"); template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^ "with _ := Induction for _ Sort _.\n", 7,10, "S"); - item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"M") + item "match" ~label:"match ..." ~accel:(modifier_for_templates#get^"M") ~callback:match_callback ]; alpha_items templates_menu "Template" Coq_commands.commands; @@ -1211,17 +1140,17 @@ let build_ui () = item "Help" ~label:"_Help"; item "Browse Coq Manual" ~label:"Browse Coq _Manual" ~callback:(fun _ -> - browse notebook#current_term.messages#add (doc_url ())); + browse notebook#current_term.messages#add_string (doc_url ())); item "Browse Coq Library" ~label:"Browse Coq _Library" ~callback:(fun _ -> - browse notebook#current_term.messages#add prefs.library_url); + browse notebook#current_term.messages#add_string library_url#get); item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP ~callback:(fun _ -> on_current_term (fun sn -> - browse_keyword sn.messages#add (get_current_word sn))); + browse_keyword sn.messages#add_string (get_current_word sn))); item "Help for μPG mode" ~label:"Help for μPG mode" ~callback:(fun _ -> on_current_term (fun sn -> sn.messages#clear; - sn.messages#add (NanoPG.get_documentation ()))); + sn.messages#add_string (NanoPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; @@ -1259,7 +1188,7 @@ let build_ui () = (* Reset on tab switch *) let _ = notebook#connect#switch_page ~callback:(fun _ -> - if prefs.reset_on_tab_switch then Nav.restart ()) + if reset_on_tab_switch#get then Nav.restart ()) in (* Vertical Separator between Scripts and Goals *) @@ -1267,7 +1196,7 @@ let build_ui () = let () = refresh_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let () = lower_hbox#pack ~expand:true status#coerce in - let () = push_info ("Ready"^ if current.nanoPG then ", [μPG]" else "") in + let () = push_info ("Ready"^ if nanoPG#get then ", [μPG]" else "") in (* Location display *) let l = GMisc.label @@ -1310,43 +1239,33 @@ let build_ui () = let _ = Glib.Timeout.add ~ms:300 ~callback in (* Initializing hooks *) - let refresh_toolbar () = - if prefs.show_toolbar - then toolbar#misc#show () - else toolbar#misc#hide () - in - let refresh_style () = - let style = style_manager#style_scheme prefs.source_style in + let refresh_style style = + let style = style_manager#style_scheme style in let iter_session v = v.script#source_buffer#set_style_scheme style in List.iter iter_session notebook#pages in - let refresh_language () = - let lang = lang_manager#language prefs.source_language in + let refresh_language lang = + let lang = lang_manager#language lang in let iter_session v = v.script#source_buffer#set_language lang in List.iter iter_session notebook#pages in - let resize_window () = - w#resize ~width:prefs.window_width ~height:prefs.window_height + let refresh_toolbar b = + if b then toolbar#misc#show () else toolbar#misc#hide () in - refresh_toolbar (); - refresh_toolbar_hook := refresh_toolbar; - refresh_style_hook := refresh_style; - refresh_language_hook := refresh_language; - refresh_editor_hook := refresh_editor_prefs; - resize_window_hook := resize_window; - refresh_tabs_hook := refresh_notebook_pos; + stick show_toolbar toolbar refresh_toolbar; + let _ = source_style#connect#changed refresh_style in + let _ = source_language#connect#changed refresh_language in (* Color configuration *) Tags.Script.incomplete#set_property (`BACKGROUND_STIPPLE (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02")); - Tags.Script.incomplete#set_property - (`BACKGROUND_GDK (Tags.get_processed_color ())); (* Showtime ! *) w#show () + (** {2 Coqide main function } *) let make_file_buffer f = @@ -1356,7 +1275,7 @@ let make_file_buffer f = let make_scratch_buffer () = let session = create_session None in let _ = notebook#append_term session in - !refresh_editor_hook () + () let main files = build_ui (); diff --git a/ide/fileOps.ml b/ide/fileOps.ml index 03b3fcd4e..eccd61d0d 100644 --- a/ide/fileOps.ml +++ b/ide/fileOps.ml @@ -8,8 +8,6 @@ open Ideutils -let prefs = Preferences.current - let revert_timer = mktimer () let autosave_timer = mktimer () @@ -87,7 +85,7 @@ object(self) flash_info "Could not overwrite file" | _ -> Minilib.log "Auto revert set to false"; - prefs.Preferences.global_auto_revert <- false; + Preferences.global_auto_revert#set false; revert_timer.kill () method save f = @@ -120,9 +118,9 @@ object(self) | None -> None | Some f -> let dir = Filename.dirname f in - let base = (fst prefs.Preferences.auto_save_name) ^ + let base = (fst Preferences.auto_save_name#get) ^ (Filename.basename f) ^ - (snd prefs.Preferences.auto_save_name) + (snd Preferences.auto_save_name#get) in Some (Filename.concat dir base) method private need_auto_save = diff --git a/ide/ide.mllib b/ide/ide.mllib index e082bd18c..83b314283 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -9,7 +9,6 @@ Configwin Editable_cells Config_parser Tags -Wg_Segment Wg_Notebook Config_lexer Utf8_convert @@ -21,6 +20,7 @@ Coq Coq_lex Sentence Gtk_parsing +Wg_Segment Wg_ProofView Wg_MessageView Wg_Detachable diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 94f9c9a36..c28ed6860 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -184,12 +184,13 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in + Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr) + in let process_hyp d (env,l) = let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in (List.fold_right Environ.push_named d' env, - (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in + (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in let (_env, hyps) = Context.fold_named_list_context process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in @@ -329,10 +330,14 @@ let handle_exn (e, info) = let loc_of e = match Loc.get_loc e with | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) | _ -> None in - let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in + let mk_msg () = + let msg = read_stdout () in + let msg = str msg ++ fnl () ++ Errors.print ~info e in + Richpp.richpp_of_pp msg + in match e with - | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" - | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" + | 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!" | e -> match Stateid.get info with | Some (valid, _) -> valid, loc_of info, mk_msg () @@ -428,12 +433,12 @@ let print_xml = let slave_logger xml_oc level message = (* convert the message into XML *) - let msg = string_of_ppcmds (hov 0 message) in + let msg = hov 0 message in let message = { Pp.message_level = level; - Pp.message_content = msg; + Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg)); } in - let () = pr_debug (Printf.sprintf "-> %S" msg) in + let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in let xml = Pp.of_message message in print_xml xml_oc xml diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 5892fb3d9..2e4adba73 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -37,7 +37,34 @@ let flash_info = let flash_context = status#new_context ~name:"Flash" in (fun ?(delay=5000) s -> flash_context#flash ~delay s) - +let xml_to_string xml = + let open Xml_datatype in + let buf = Buffer.create 1024 in + let rec iter = function + | PCData s -> Buffer.add_string buf s + | Element (_, _, children) -> + List.iter iter children + in + let () = iter (Richpp.repr xml) in + Buffer.contents buf + +let translate s = s + +let insert_xml ?(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 rec insert tags = function + | PCData s -> buf#insert ~tags:(List.rev 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 set_location = ref (function s -> failwith "not ready") @@ -74,7 +101,7 @@ let do_convert s = in let s = if Glib.Utf8.validate s then (Minilib.log "Input is UTF-8"; s) - else match current.encoding with + else match encoding#get with |Preferences.Eutf8 | Preferences.Elocale -> from_loc () |Emanual enc -> try from_manual enc with _ -> from_loc () in @@ -90,7 +117,7 @@ Please choose a correct encoding in the preference panel.*)";; let try_export file_name s = let s = - try match current.encoding with + try match encoding#get with |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s |Elocale -> let is_unicode,char_set = Glib.Convert.get_charset () in @@ -140,7 +167,7 @@ let filter_coq_files () = GFile.filter ~name:"Coq source code" ~patterns:[ "*.v"] () -let current_dir () = match current.project_path with +let current_dir () = match project_path#get with | None -> "" | Some dir -> dir @@ -164,7 +191,7 @@ let select_file_for_open ~title ?filename () = match file_chooser#filename with | None -> None | Some _ as f -> - current.project_path <- file_chooser#current_folder; f + project_path#set file_chooser#current_folder; f end | `DELETE_EVENT | `CANCEL -> None in file_chooser#destroy (); @@ -193,7 +220,7 @@ let select_file_for_save ~title ?filename () = file := file_chooser#filename; match !file with None -> () - | Some s -> current.project_path <- file_chooser#current_folder + | Some s -> project_path#set file_chooser#current_folder end | `DELETE_EVENT | `CANCEL -> () end ; @@ -238,7 +265,7 @@ let coqtop_path () = let file = match !custom_coqtop with | Some s -> s | None -> - match current.cmd_coqtop with + match cmd_coqtop#get with | Some s -> s | None -> let prog = String.copy Sys.executable_name in @@ -272,7 +299,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Pp.message_level -> string -> unit +type logger = Pp.message_level -> Richpp.richpp -> unit let default_logger level message = let level = match level with @@ -282,7 +309,7 @@ let default_logger level message = | Pp.Warning -> `WARNING | Pp.Error -> `ERROR in - Minilib.log ~level message + Minilib.log ~level (xml_to_string message) (** {6 File operations} *) @@ -364,7 +391,7 @@ let run_command display finally cmd = (** Web browsing *) let browse prerr url = - let com = Util.subst_command_placeholder current.cmd_browse url in + let com = Util.subst_command_placeholder cmd_browse#get url in let finally = function | Unix.WEXITED 127 -> prerr @@ -375,13 +402,13 @@ let browse prerr url = run_command (fun _ -> ()) finally com let doc_url () = - if current.doc_url = use_default_doc_url || current.doc_url = "" + if doc_url#get = use_default_doc_url || doc_url#get = "" then let addr = List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";"index.html"] in if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman - else current.doc_url + else doc_url#get let url_for_keyword = let ht = Hashtbl.create 97 in diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 1fb30e4d7..db2dce5a3 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -52,6 +52,11 @@ val pop_info : unit -> unit val clear_info : unit -> unit val flash_info : ?delay:int -> string -> unit +val xml_to_string : Richpp.richpp -> string + +val insert_xml : ?tags:GText.tag list -> + #GText.buffer_skel -> Richpp.richpp -> unit + val set_location : (string -> unit) ref (* In win32, when a command-line is to be executed via cmd.exe @@ -64,9 +69,9 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Pp.message_level -> string -> unit +type logger = Pp.message_level -> Richpp.richpp -> unit -val default_logger : Pp.message_level -> string -> unit +val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) (** {6 I/O operations} *) diff --git a/ide/interface.mli b/ide/interface.mli index 464e851f6..f3777ba36 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -12,14 +12,15 @@ type raw = bool type verbose = bool +type richpp = Richpp.richpp (** The type of coqtop goals *) type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : string list; + goal_hyp : richpp list; (** List of hypotheses *) - goal_ccl : string; + goal_ccl : richpp; (** Goal conclusion *) } @@ -117,7 +118,7 @@ type edit_id = Feedback.edit_id should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * string) + | Fail of (state_id * location * richpp) type ('a, 'b) union = ('a, 'b) Util.union @@ -201,7 +202,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * string +type handle_exn_rty = state_id * location * richpp (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 805ace935..0668ad09f 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -303,7 +303,7 @@ let init w nb ags = then false else begin eprintf "got key %s\n%!" (pr_key t); - if current.nanoPG then begin + if nanoPG#get then begin match find gui !cur t with | `Do e -> eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status); diff --git a/ide/preferences.ml b/ide/preferences.ml index 90862d064..23426cad6 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -17,19 +17,66 @@ let style_manager = GSourceView2.source_style_scheme_manager ~default:true let () = style_manager#set_search_path ((Minilib.coqide_data_dirs ())@style_manager#search_path) -let get_config_file name = - let find_config dir = Sys.file_exists (Filename.concat dir name) in - let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in - Filename.concat config_dir name +type tag = { + tag_fg_color : string option; + tag_bg_color : string option; + tag_bold : bool; + tag_italic : bool; + tag_underline : bool; +} -(* Small hack to handle v8.3 to v8.4 change in configuration file *) -let loaded_pref_file = - try get_config_file "coqiderc" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc" +(** Generic preferences *) -let loaded_accel_file = - try get_config_file "coqide.keys" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" +type obj = { + set : string list -> unit; + get : unit -> string list; +} + +let preferences : obj Util.String.Map.t ref = ref Util.String.Map.empty + +class type ['a] repr = +object + method into : string list -> 'a option + method from : 'a -> string list +end + +class ['a] preference_signals ~(changed : 'a GUtil.signal) = +object + inherit GUtil.ml_signals [changed#disconnect] + method changed = changed#connect ~after +end + +class ['a] preference ~(name : string list) ~(init : 'a) ~(repr : 'a repr) = +object (self) + initializer + let set v = match repr#into v with None -> () | Some s -> self#set s in + let get () = repr#from self#get in + let obj = { set = set; get = get; } in + let name = String.concat "." name in + if Util.String.Map.mem name !preferences then + invalid_arg ("Preference " ^ name ^ " already exists") + else + preferences := Util.String.Map.add name obj !preferences + + val default = init + val mutable data = init + val changed : 'a GUtil.signal = new GUtil.signal () + val name : string list = name + method connect = new preference_signals ~changed + method get = data + method set (n : 'a) = data <- n; changed#call n + method reset () = self#set default + method default = default +end + +let stick (pref : 'a preference) (obj : #GObj.widget as 'obj) + (cb : 'a -> unit) = + let _ = cb pref#get in + let p_id = pref#connect#changed (fun v -> cb v) in + let _ = obj#misc#connect#destroy (fun () -> pref#connect#disconnect p_id) in + () + +(** Useful marshallers *) let mod_to_str m = match m with @@ -74,359 +121,502 @@ let inputenc_of_string s = else if s = "LOCALE" then Elocale else Emanual s) +let use_default_doc_url = "(automatic)" + +module Repr = +struct + +let string : string repr = +object + method from s = [s] + method into = function [s] -> Some s | _ -> None +end + +let string_pair : (string * string) repr = +object + method from (s1, s2) = [s1; s2] + method into = function [s1; s2] -> Some (s1, s2) | _ -> None +end + +let string_list : string list repr = +object + method from s = s + method into s = Some s +end + +let bool : bool repr = +object + method from s = [string_of_bool s] + method into = function + | ["true"] -> Some true + | ["false"] -> Some false + | _ -> None +end + +let int : int repr = +object + method from s = [string_of_int s] + method into = function + | [i] -> (try Some (int_of_string i) with _ -> None) + | _ -> None +end + +let option (r : 'a repr) : 'a option repr = +object + method from = function None -> [] | Some v -> "" :: r#from v + method into = function + | [] -> Some None + | "" :: s -> Some (r#into s) + | _ -> None +end + +let custom (from : 'a -> string) (into : string -> 'a) : 'a repr = +object + method from x = try [from x] with _ -> [] + method into = function + | [s] -> (try Some (into s) with _ -> None) + | _ -> None +end + +let tag : tag repr = +let _to s = if s = "" then None else Some s in +let _of = function None -> "" | Some s -> s in +object + method from tag = [ + _of tag.tag_fg_color; + _of tag.tag_bg_color; + string_of_bool tag.tag_bold; + string_of_bool tag.tag_italic; + string_of_bool tag.tag_underline; + ] + method into = function + | [fg; bg; bd; it; ul] -> + (try Some { + tag_fg_color = _to fg; + tag_bg_color = _to bg; + tag_bold = bool_of_string bd; + tag_italic = bool_of_string it; + tag_underline = bool_of_string ul; + } + with _ -> None) + | _ -> None +end + +end + +let get_config_file name = + let find_config dir = Sys.file_exists (Filename.concat dir name) in + let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in + Filename.concat config_dir name + +(* Small hack to handle v8.3 to v8.4 change in configuration file *) +let loaded_pref_file = + try get_config_file "coqiderc" + with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc" + +let loaded_accel_file = + try get_config_file "coqide.keys" + with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" (** Hooks *) -let refresh_style_hook = ref (fun () -> ()) -let refresh_language_hook = ref (fun () -> ()) -let refresh_editor_hook = ref (fun () -> ()) -let refresh_toolbar_hook = ref (fun () -> ()) -let contextual_menus_on_goal_hook = ref (fun x -> ()) -let resize_window_hook = ref (fun () -> ()) -let refresh_tabs_hook = ref (fun () -> ()) +(** New style preferences *) -type pref = - { - mutable cmd_coqtop : string option; - mutable cmd_coqc : string; - mutable cmd_make : string; - mutable cmd_coqmakefile : string; - mutable cmd_coqdoc : string; +let cmd_coqtop = + new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string) - mutable source_language : string; - mutable source_style : string; +let cmd_coqc = + new preference ~name:["cmd_coqc"] ~init:"coqc" ~repr:Repr.(string) - mutable global_auto_revert : bool; - mutable global_auto_revert_delay : int; +let cmd_make = + new preference ~name:["cmd_make"] ~init:"make" ~repr:Repr.(string) - mutable auto_save : bool; - mutable auto_save_delay : int; - mutable auto_save_name : string * string; +let cmd_coqmakefile = + new preference ~name:["cmd_coqmakefile"] ~init:"coq_makefile -o makefile *.v" ~repr:Repr.(string) - mutable read_project : project_behavior; - mutable project_file_name : string; - mutable project_path : string option; +let cmd_coqdoc = + new preference ~name:["cmd_coqdoc"] ~init:"coqdoc -q -g" ~repr:Repr.(string) - mutable encoding : inputenc; +let source_language = + new preference ~name:["source_language"] ~init:"coq" ~repr:Repr.(string) - mutable automatic_tactics : string list; - mutable cmd_print : string; +let source_style = + new preference ~name:["source_style"] ~init:"coq_style" ~repr:Repr.(string) - mutable modifier_for_navigation : string; - mutable modifier_for_templates : string; - mutable modifier_for_tactics : string; - mutable modifier_for_display : string; - mutable modifiers_valid : string; +let global_auto_revert = + new preference ~name:["global_auto_revert"] ~init:false ~repr:Repr.(bool) - mutable cmd_browse : string; - mutable cmd_editor : string; +let global_auto_revert_delay = + new preference ~name:["global_auto_revert_delay"] ~init:10000 ~repr:Repr.(int) - mutable text_font : Pango.font_description; +let auto_save = + new preference ~name:["auto_save"] ~init:true ~repr:Repr.(bool) - mutable doc_url : string; - mutable library_url : string; +let auto_save_delay = + new preference ~name:["auto_save_delay"] ~init:10000 ~repr:Repr.(int) - mutable show_toolbar : bool; - mutable contextual_menus_on_goal : bool; - mutable window_width : int; - mutable window_height :int; - mutable query_window_width : int; - mutable query_window_height : int; -(* - mutable use_utf8_notation : bool; -*) - mutable auto_complete : bool; - mutable stop_before : bool; - mutable reset_on_tab_switch : bool; - mutable vertical_tabs : bool; - mutable opposite_tabs : bool; - - mutable background_color : string; - mutable processing_color : string; - mutable processed_color : string; - mutable error_color : string; - mutable error_fg_color : string; - - mutable dynamic_word_wrap : bool; - mutable show_line_number : bool; - mutable auto_indent : bool; - mutable show_spaces : bool; - mutable show_right_margin : bool; - mutable show_progress_bar : bool; - mutable spaces_instead_of_tabs : bool; - mutable tab_length : int; - mutable highlight_current_line : bool; - - mutable nanoPG : bool; +let auto_save_name = + new preference ~name:["auto_save_name"] ~init:("#","#") ~repr:Repr.(string_pair) -} +let read_project = + let repr = Repr.custom string_of_project_behavior project_behavior_of_string in + new preference ~name:["read_project"] ~init:Append_args ~repr -let use_default_doc_url = "(automatic)" +let project_file_name = + new preference ~name:["project_file_name"] ~init:"_CoqProject" ~repr:Repr.(string) -let current = { - cmd_coqtop = None; - cmd_coqc = "coqc"; - cmd_make = "make"; - cmd_coqmakefile = "coq_makefile -o makefile *.v"; - cmd_coqdoc = "coqdoc -q -g"; - cmd_print = "lpr"; +let project_path = + new preference ~name:["project_path"] ~init:None ~repr:Repr.(option string) - global_auto_revert = false; - global_auto_revert_delay = 10000; +let encoding = + let repr = Repr.custom string_of_inputenc inputenc_of_string in + let init = if Sys.os_type = "Win32" then Eutf8 else Elocale in + new preference ~name:["encoding"] ~init ~repr - auto_save = true; - auto_save_delay = 10000; - auto_save_name = "#","#"; +let automatic_tactics = + let init = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ] in + new preference ~name:["automatic_tactics"] ~init ~repr:Repr.(string_list) - source_language = "coq"; - source_style = "coq_style"; +let cmd_print = + new preference ~name:["cmd_print"] ~init:"lpr" ~repr:Repr.(string) - read_project = Append_args; - project_file_name = "_CoqProject"; - project_path = None; +let attach_modifiers (pref : string preference) prefix = + let cb mds = + let mds = str_to_mod_list mds in + let change ~path ~key ~modi ~changed = + if CString.is_sub prefix path 0 then + ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path) + in + GtkData.AccelMap.foreach change + in + pref#connect#changed cb - encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; +let modifier_for_navigation = + new preference ~name:["modifier_for_navigation"] ~init:"<Control>" ~repr:Repr.(string) - automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; - "auto with *"; "intuition" ]; +let modifier_for_templates = + new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string) + +let modifier_for_tactics = + new preference ~name:["modifier_for_tactics"] ~init:"<Control><Alt>" ~repr:Repr.(string) - modifier_for_navigation = "<Control>"; - modifier_for_templates = "<Control><Shift>"; - modifier_for_tactics = "<Control><Alt>"; - modifier_for_display = "<Alt><Shift>"; - modifiers_valid = "<Alt><Control><Shift>"; +let modifier_for_display = + new preference ~name:["modifier_for_display"] ~init:"<Alt><Shift>" ~repr:Repr.(string) +let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" +let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" +let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" +let _ = attach_modifiers modifier_for_display "<Actions>/View/" - cmd_browse = Flags.browser_cmd_fmt; - cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s"; +let modifiers_valid = + new preference ~name:["modifiers_valid"] ~init:"<Alt><Control><Shift>" ~repr:Repr.(string) -(* text_font = Pango.Font.from_string "sans 12";*) - text_font = Pango.Font.from_string (match Coq_config.gtk_platform with - |`QUARTZ -> "Arial Unicode MS 11" - |_ -> "Monospace 10"); +let cmd_browse = + new preference ~name:["cmd_browse"] ~init:Flags.browser_cmd_fmt ~repr:Repr.(string) - doc_url = Coq_config.wwwrefman; - library_url = Coq_config.wwwstdlib; +let cmd_editor = + let init = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s" in + new preference ~name:["cmd_editor"] ~init ~repr:Repr.(string) - show_toolbar = true; - contextual_menus_on_goal = true; - window_width = 800; - window_height = 600; - query_window_width = 600; - query_window_height = 400; -(* - use_utf8_notation = false; -*) - auto_complete = false; - stop_before = true; - reset_on_tab_switch = false; - vertical_tabs = false; - opposite_tabs = false; - - background_color = Tags.default_color; - processed_color = Tags.default_processed_color; - processing_color = Tags.default_processing_color; - error_color = Tags.default_error_color; - error_fg_color = Tags.default_error_fg_color; - - dynamic_word_wrap = false; - show_line_number = false; - auto_indent = false; - show_spaces = true; - show_right_margin = false; - show_progress_bar = true; - spaces_instead_of_tabs = true; - tab_length = 2; - highlight_current_line = false; - - nanoPG = false; - } +let text_font = + let init = match Coq_config.gtk_platform with + | `QUARTZ -> "Arial Unicode MS 11" + | _ -> "Monospace 10" + in + new preference ~name:["text_font"] ~init ~repr:Repr.(string) + +let doc_url = +object + inherit [string] preference + ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string) + as super + + method set v = + if not (Flags.is_standard_doc_url v) && + v <> use_default_doc_url && + (* Extra hack to support links to last released doc version *) + v <> Coq_config.wwwcoq ^ "doc" && + v <> Coq_config.wwwcoq ^ "doc/" + then super#set v + +end + +let library_url = + new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string) + +let show_toolbar = + new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool) + +let contextual_menus_on_goal = + new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool) + +let window_width = + new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int) + +let window_height = + new preference ~name:["window_height"] ~init:600 ~repr:Repr.(int) + +let auto_complete = + new preference ~name:["auto_complete"] ~init:false ~repr:Repr.(bool) + +let stop_before = + new preference ~name:["stop_before"] ~init:true ~repr:Repr.(bool) + +let reset_on_tab_switch = + new preference ~name:["reset_on_tab_switch"] ~init:false ~repr:Repr.(bool) + +let vertical_tabs = + new preference ~name:["vertical_tabs"] ~init:false ~repr:Repr.(bool) + +let opposite_tabs = + new preference ~name:["opposite_tabs"] ~init:false ~repr:Repr.(bool) + +let background_color = + new preference ~name:["background_color"] ~init:"cornsilk" ~repr:Repr.(string) + +let attach_bg (pref : string preference) (tag : GText.tag) = + pref#connect#changed (fun c -> tag#set_property (`BACKGROUND c)) + +let attach_fg (pref : string preference) (tag : GText.tag) = + pref#connect#changed (fun c -> tag#set_property (`FOREGROUND c)) + +let processing_color = + new preference ~name:["processing_color"] ~init:"light blue" ~repr:Repr.(string) + +let _ = attach_bg processing_color Tags.Script.to_process +let _ = attach_bg processing_color Tags.Script.incomplete + +let default_tag = { + tag_fg_color = None; + tag_bg_color = None; + tag_bold = false; + tag_italic = false; + tag_underline = false; +} + +let tags = ref Util.String.Map.empty + +let list_tags () = !tags + +let create_tag name default = + let pref = new preference ~name:[name] ~init:default ~repr:Repr.(tag) in + let set_tag tag = + begin match pref#get.tag_bg_color with + | None -> tag#set_property (`BACKGROUND_SET false) + | Some c -> + tag#set_property (`BACKGROUND_SET true); + tag#set_property (`BACKGROUND c) + end; + begin match pref#get.tag_fg_color with + | None -> tag#set_property (`FOREGROUND_SET false) + | Some c -> + tag#set_property (`FOREGROUND_SET true); + tag#set_property (`FOREGROUND c) + end; + begin match pref#get.tag_bold with + | false -> tag#set_property (`WEIGHT_SET false) + | true -> + tag#set_property (`WEIGHT_SET true); + tag#set_property (`WEIGHT `BOLD) + end; + begin match pref#get.tag_italic with + | false -> tag#set_property (`STYLE_SET false) + | true -> + tag#set_property (`STYLE_SET true); + tag#set_property (`STYLE `ITALIC) + end; + begin match pref#get.tag_underline with + | false -> tag#set_property (`UNDERLINE_SET false) + | true -> + tag#set_property (`UNDERLINE_SET true); + tag#set_property (`UNDERLINE `SINGLE) + end; + in + let iter table = + let tag = GText.tag ~name () in + table#add tag#as_tag; + pref#connect#changed (fun _ -> set_tag tag); + set_tag tag; + in + List.iter iter [Tags.Script.table; Tags.Proof.table; Tags.Message.table]; + tags := Util.String.Map.add name pref !tags + +let () = + let iter name = create_tag name default_tag in + List.iter iter [ + "constr.evar"; + "constr.keyword"; + "constr.notation"; + "constr.path"; + "constr.reference"; + "constr.type"; + "constr.variable"; + "message.debug"; + "message.error"; + "message.warning"; + "module.definition"; + "module.keyword"; + "tactic.keyword"; + "tactic.primitive"; + "tactic.string"; + ] + +let processed_color = + new preference ~name:["processed_color"] ~init:"light green" ~repr:Repr.(string) + +let _ = attach_bg processed_color Tags.Script.processed +let _ = attach_bg processed_color Tags.Proof.highlight + +let error_color = + new preference ~name:["error_color"] ~init:"#FFCCCC" ~repr:Repr.(string) + +let _ = attach_bg error_color Tags.Script.error_bg + +let error_fg_color = + new preference ~name:["error_fg_color"] ~init:"red" ~repr:Repr.(string) + +let _ = attach_fg error_fg_color Tags.Script.error + +let dynamic_word_wrap = + new preference ~name:["dynamic_word_wrap"] ~init:false ~repr:Repr.(bool) + +let show_line_number = + new preference ~name:["show_line_number"] ~init:false ~repr:Repr.(bool) + +let auto_indent = + new preference ~name:["auto_indent"] ~init:false ~repr:Repr.(bool) + +let show_spaces = + new preference ~name:["show_spaces"] ~init:true ~repr:Repr.(bool) + +let show_right_margin = + new preference ~name:["show_right_margin"] ~init:false ~repr:Repr.(bool) + +let show_progress_bar = + new preference ~name:["show_progress_bar"] ~init:true ~repr:Repr.(bool) + +let spaces_instead_of_tabs = + new preference ~name:["spaces_instead_of_tabs"] ~init:true ~repr:Repr.(bool) + +let tab_length = + new preference ~name:["tab_length"] ~init:2 ~repr:Repr.(int) + +let highlight_current_line = + new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool) + +let nanoPG = + new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) + +class tag_button (box : Gtk.box Gtk.obj) = +object (self) + + inherit GObj.widget box + + val fg_color = GButton.color_button () + val fg_unset = GButton.toggle_button () + val bg_color = GButton.color_button () + val bg_unset = GButton.toggle_button () + val bold = GButton.toggle_button () + val italic = GButton.toggle_button () + val underline = GButton.toggle_button () + + method set_tag tag = + let track c but set = match c with + | None -> set#set_active true + | Some c -> + set#set_active false; + but#set_color (Tags.color_of_string c) + in + track tag.tag_bg_color bg_color bg_unset; + track tag.tag_fg_color fg_color fg_unset; + bold#set_active tag.tag_bold; + italic#set_active tag.tag_italic; + underline#set_active tag.tag_underline; + + method tag = + let get but set = + if set#active then None + else Some (Tags.string_of_color but#color) + in + { + tag_bg_color = get bg_color bg_unset; + tag_fg_color = get fg_color fg_unset; + tag_bold = bold#active; + tag_italic = italic#active; + tag_underline = underline#active; + } + + initializer + let box = new GPack.box box in + let set_stock button stock = + let stock = GMisc.image ~stock ~icon_size:`BUTTON () in + button#set_image stock#coerce + in + set_stock fg_unset `CANCEL; + set_stock bg_unset `CANCEL; + set_stock bold `BOLD; + set_stock italic `ITALIC; + set_stock underline `UNDERLINE; + box#pack fg_color#coerce; + box#pack fg_unset#coerce; + box#pack bg_color#coerce; + box#pack bg_unset#coerce; + box#pack bold#coerce; + box#pack italic#coerce; + box#pack underline#coerce; + let cb but obj = obj#set_sensitive (not but#active) in + let _ = fg_unset#connect#toggled (fun () -> cb fg_unset fg_color#misc) in + let _ = bg_unset#connect#toggled (fun () -> cb bg_unset bg_color#misc) in + () + +end + +let tag_button () = + let box = GPack.hbox () in + new tag_button (Gobject.unsafe_cast box#as_widget) + +(** Old style preferences *) let save_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; let () = try GtkData.AccelMap.save accel_file with _ -> () in - let p = current in - - let add = Util.String.Map.add in - let (++) x f = f x in - Util.String.Map.empty ++ - add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++ - add "cmd_coqc" [p.cmd_coqc] ++ - add "cmd_make" [p.cmd_make] ++ - add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ - add "cmd_coqdoc" [p.cmd_coqdoc] ++ - add "source_language" [p.source_language] ++ - add "source_style" [p.source_style] ++ - add "global_auto_revert" [string_of_bool p.global_auto_revert] ++ - 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] ++ - add "auto_save_name" [fst p.auto_save_name; snd p.auto_save_name] ++ - - add "project_options" [string_of_project_behavior p.read_project] ++ - add "project_file_name" [p.project_file_name] ++ - add "project_path" (match p.project_path with None -> [] | Some s -> [s]) ++ - - add "encoding" [string_of_inputenc p.encoding] ++ - - add "automatic_tactics" p.automatic_tactics ++ - add "cmd_print" [p.cmd_print] ++ - add "modifier_for_navigation" [p.modifier_for_navigation] ++ - add "modifier_for_templates" [p.modifier_for_templates] ++ - add "modifier_for_tactics" [p.modifier_for_tactics] ++ - add "modifier_for_display" [p.modifier_for_display] ++ - add "modifiers_valid" [p.modifiers_valid] ++ - add "cmd_browse" [p.cmd_browse] ++ - add "cmd_editor" [p.cmd_editor] ++ - - add "text_font" [Pango.Font.to_string p.text_font] ++ - - 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" - [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] ++ - add "query_window_height" [string_of_int p.query_window_height] ++ - add "query_window_width" [string_of_int p.query_window_width] ++ - add "auto_complete" [string_of_bool p.auto_complete] ++ - add "stop_before" [string_of_bool p.stop_before] ++ - add "reset_on_tab_switch" [string_of_bool p.reset_on_tab_switch] ++ - add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ - add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ - add "background_color" [p.background_color] ++ - add "processing_color" [p.processing_color] ++ - add "processed_color" [p.processed_color] ++ - add "error_color" [p.error_color] ++ - add "error_fg_color" [p.error_fg_color] ++ - add "dynamic_word_wrap" [string_of_bool p.dynamic_word_wrap] ++ - add "show_line_number" [string_of_bool p.show_line_number] ++ - add "auto_indent" [string_of_bool p.auto_indent] ++ - add "show_spaces" [string_of_bool p.show_spaces] ++ - add "show_right_margin" [string_of_bool p.show_right_margin] ++ - add "show_progress_bar" [string_of_bool p.show_progress_bar] ++ - add "spaces_instead_of_tabs" [string_of_bool p.spaces_instead_of_tabs] ++ - add "tab_length" [string_of_int p.tab_length] ++ - add "highlight_current_line" [string_of_bool p.highlight_current_line] ++ - add "nanoPG" [string_of_bool p.nanoPG] ++ + 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 load_pref () = let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let m = Config_lexer.load_file loaded_pref_file in - let np = current in - let set k f = try let v = Util.String.Map.find k m in f v with _ -> () in - let set_hd k f = set k (fun v -> f (List.hd v)) in - 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 = - set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) + let iter name v = + try (Util.String.Map.find name !preferences).set v + with _ -> () in - let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ -> Some h)) in - set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v); - set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); - set_hd "cmd_make" (fun v -> np.cmd_make <- v); - set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); - set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v); - set_hd "source_language" (fun v -> np.source_language <- v); - set_hd "source_style" (fun v -> np.source_style <- v); - set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v); - 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); - set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2)); - set_hd "encoding" (fun v -> np.encoding <- (inputenc_of_string v)); - set_hd "project_options" - (fun v -> np.read_project <- (project_behavior_of_string v)); - set_hd "project_file_name" (fun v -> np.project_file_name <- v); - set_option "project_path" (fun v -> np.project_path <- v); - set "automatic_tactics" - (fun v -> np.automatic_tactics <- v); - set_hd "cmd_print" (fun v -> np.cmd_print <- v); - set_hd "modifier_for_navigation" - (fun v -> np.modifier_for_navigation <- v); - set_hd "modifier_for_templates" - (fun v -> np.modifier_for_templates <- v); - set_hd "modifier_for_tactics" - (fun v -> np.modifier_for_tactics <- v); - set_hd "modifier_for_display" - (fun v -> np.modifier_for_display <- v); - set_hd "modifiers_valid" - (fun v -> - np.modifiers_valid <- 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 -> - if not (Flags.is_standard_doc_url v) && - v <> use_default_doc_url && - (* Extra hack to support links to last released doc version *) - v <> Coq_config.wwwcoq ^ "doc" && - v <> Coq_config.wwwcoq ^ "doc/" - then - (* ("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" - (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); - set_int "query_window_width" (fun v -> np.query_window_width <- v); - set_int "query_window_height" (fun v -> np.query_window_height <- v); - set_bool "auto_complete" (fun v -> np.auto_complete <- v); - set_bool "stop_before" (fun v -> np.stop_before <- v); - set_bool "reset_on_tab_switch" (fun v -> np.reset_on_tab_switch <- v); - set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); - set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); - set_hd "background_color" (fun v -> np.background_color <- v); - set_hd "processing_color" (fun v -> np.processing_color <- v); - set_hd "processed_color" (fun v -> np.processed_color <- v); - set_hd "error_color" (fun v -> np.error_color <- v); - set_hd "error_fg_color" (fun v -> np.error_fg_color <- v); - set_bool "dynamic_word_wrap" (fun v -> np.dynamic_word_wrap <- v); - set_bool "show_line_number" (fun v -> np.show_line_number <- v); - set_bool "auto_indent" (fun v -> np.auto_indent <- v); - set_bool "show_spaces" (fun v -> np.show_spaces <- v); - set_bool "show_right_margin" (fun v -> np.show_right_margin <- v); - set_bool "show_progress_bar" (fun v -> np.show_progress_bar <- v); - set_bool "spaces_instead_of_tabs" (fun v -> np.spaces_instead_of_tabs <- v); - set_int "tab_length" (fun v -> np.tab_length <- v); - set_bool "highlight_current_line" (fun v -> np.highlight_current_line <- v); - set_bool "nanoPG" (fun v -> np.nanoPG <- v); - () + Util.String.Map.iter iter m + +let pstring name p = string ~f:p#set name p#get +let pbool name p = bool ~f:p#set name p#get +let pmodifiers ?(all = false) name p = modifiers + ?allow:(if all then None else Some (str_to_mod_list modifiers_valid#get)) + ~f:(fun l -> p#set (mod_list_to_str l)) + ~help:"restart to apply" + name + (str_to_mod_list p#get) let configure ?(apply=(fun () -> ())) () = let cmd_coqtop = string - ~f:(fun s -> current.cmd_coqtop <- if s = "AUTO" then None else Some s) - " coqtop" (match current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in - let cmd_coqc = - string - ~f:(fun s -> current.cmd_coqc <- s) - " coqc" current.cmd_coqc in - let cmd_make = - string - ~f:(fun s -> current.cmd_make <- s) - " make" current.cmd_make in - let cmd_coqmakefile = - string - ~f:(fun s -> current.cmd_coqmakefile <- s) - "coqmakefile" current.cmd_coqmakefile in - 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) - " Print ps" current.cmd_print in + ~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s)) + " coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in + let cmd_coqc = pstring " coqc" cmd_coqc in + let cmd_make = pstring " make" cmd_make in + let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in + let cmd_coqdoc = pstring " coqdoc" cmd_coqdoc in + let cmd_print = pstring " Print ps" cmd_print in let config_font = let box = GPack.hbox () in @@ -435,18 +625,13 @@ let configure ?(apply=(fun () -> ())) () = "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; box#pack ~expand:true w#coerce; ignore (w#misc#connect#realize - ~callback:(fun () -> w#set_font_name - (Pango.Font.to_string current.text_font))); + ~callback:(fun () -> w#set_font_name text_font#get)); custom ~label:"Fonts for text" box (fun () -> let fd = w#font_name in - current.text_font <- (Pango.Font.from_string fd) ; -(* - Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string current.text_font); -*) - !refresh_editor_hook ()) + text_font#set fd) true in @@ -458,121 +643,98 @@ let configure ?(apply=(fun () -> ())) () = ~border_width:2 ~packing:(box#pack ~expand:true) () in - let background_label = GMisc.label - ~text:"Background color" - ~packing:(table#attach ~expand:`X ~left:0 ~top:0) () - in - let processed_label = GMisc.label - ~text:"Background color of processed text" - ~packing:(table#attach ~expand:`X ~left:0 ~top:1) () - in - let processing_label = GMisc.label - ~text:"Background color of text being processed" - ~packing:(table#attach ~expand:`X ~left:0 ~top:2) () - in - let error_label = GMisc.label - ~text:"Background color of errors" - ~packing:(table#attach ~expand:`X ~left:0 ~top:3) () - in - let error_fg_label = GMisc.label - ~text:"Foreground color of errors" - ~packing:(table#attach ~expand:`X ~left:0 ~top:4) () - in - let () = background_label#set_xalign 0. in - let () = processed_label#set_xalign 0. in - let () = processing_label#set_xalign 0. in - let () = error_label#set_xalign 0. in - let () = error_fg_label#set_xalign 0. in - let background_button = GButton.color_button - ~color:(Tags.color_of_string (current.background_color)) - ~packing:(table#attach ~left:1 ~top:0) () - in - let processed_button = GButton.color_button - ~color:(Tags.get_processed_color ()) - ~packing:(table#attach ~left:1 ~top:1) () + let reset_button = GButton.button + ~label:"Reset" + ~packing:box#pack () in - let processing_button = GButton.color_button - ~color:(Tags.get_processing_color ()) - ~packing:(table#attach ~left:1 ~top:2) () + let iter i (text, pref) = + let label = GMisc.label + ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:i) () + in + let () = label#set_xalign 0. in + let button = GButton.color_button + ~color:(Tags.color_of_string pref#get) + ~packing:(table#attach ~left:1 ~top:i) () + in + let _ = button#connect#color_set begin fun () -> + pref#set (Tags.string_of_color button#color) + end in + let reset _ = + pref#reset (); + button#set_color Tags.(color_of_string pref#get) + in + let _ = reset_button#connect#clicked ~callback:reset in + () in - let error_button = GButton.color_button - ~color:(Tags.get_error_color ()) - ~packing:(table#attach ~left:1 ~top:3) () + let () = Util.List.iteri iter [ + ("Background color", background_color); + ("Background color of processed text", processed_color); + ("Background color of text being processed", processing_color); + ("Background color of errors", error_color); + ("Foreground color of errors", error_fg_color); + ] in + let label = "Color configuration" in + let callback () = () in + custom ~label box callback true + in + + let config_tags = + let box = GPack.vbox () in + let scroll = GBin.scrolled_window + ~hpolicy:`NEVER + ~vpolicy:`AUTOMATIC + ~packing:(box#pack ~expand:true) + () in - let error_fg_button = GButton.color_button - ~color:(Tags.get_error_fg_color ()) - ~packing:(table#attach ~left:1 ~top:4) () + let table = GPack.table + ~row_spacings:5 + ~col_spacings:5 + ~border_width:2 + ~packing:scroll#add_with_viewport () in let reset_button = GButton.button ~label:"Reset" ~packing:box#pack () in - let reset_cb () = - background_button#set_color Tags.(color_of_string default_color); - processing_button#set_color Tags.(color_of_string default_processing_color); - processed_button#set_color Tags.(color_of_string default_processed_color); - error_button#set_color Tags.(color_of_string default_error_color); - in - let _ = reset_button#connect#clicked ~callback:reset_cb in - let label = "Color configuration" in - let callback () = - current.background_color <- Tags.string_of_color background_button#color; - current.processing_color <- Tags.string_of_color processing_button#color; - current.processed_color <- Tags.string_of_color processed_button#color; - current.error_color <- Tags.string_of_color error_button#color; - current.error_fg_color <- Tags.string_of_color error_fg_button#color; - !refresh_editor_hook (); - Tags.set_processing_color processing_button#color; - Tags.set_processed_color processed_button#color; - Tags.set_error_color error_button#color; - Tags.set_error_fg_color error_fg_button#color + let i = ref 0 in + let cb = ref [] in + let iter text tag = + let label = GMisc.label + ~text ~packing:(table#attach ~expand:`X ~left:0 ~top:!i) () + in + let () = label#set_xalign 0. in + let button = tag_button () in + let callback () = tag#set button#tag in + button#set_tag tag#get; + table#attach ~left:1 ~top:!i button#coerce; + incr i; + cb := callback :: !cb; in + let () = Util.String.Map.iter iter !tags in + let label = "Tag configuration" in + let callback () = List.iter (fun f -> f ()) !cb in custom ~label box callback true in let config_editor = let label = "Editor configuration" in let box = GPack.vbox () in - let gen_button text active = - GButton.check_button ~label:text ~active ~packing:box#pack () in - let wrap = gen_button "Dynamic word wrap" current.dynamic_word_wrap in - let line = gen_button "Show line number" current.show_line_number in - let auto_indent = gen_button "Auto indentation" current.auto_indent in - let auto_complete = gen_button "Auto completion" current.auto_complete in - let show_spaces = gen_button "Show spaces" current.show_spaces in - let show_right_margin = gen_button "Show right margin" current.show_right_margin in - let show_progress_bar = gen_button "Show progress bar" current.show_progress_bar in - let spaces_instead_of_tabs = - gen_button "Insert spaces instead of tabs" - current.spaces_instead_of_tabs - in - let highlight_current_line = - gen_button "Highlight current line" - current.highlight_current_line - in - let nanoPG = gen_button "Emacs/PG keybindings (μPG mode)" current.nanoPG in -(* let lbox = GPack.hbox ~packing:box#pack () in *) -(* let _ = GMisc.label ~text:"Tab width" *) -(* ~xalign:0. *) -(* ~packing:(lbox#pack ~expand:true) () *) -(* in *) -(* let tab_width = GEdit.spin_button *) -(* ~digits:0 ~packing:lbox#pack () *) -(* in *) - let callback () = - current.dynamic_word_wrap <- wrap#active; - current.show_line_number <- line#active; - current.auto_indent <- auto_indent#active; - current.show_spaces <- show_spaces#active; - current.show_right_margin <- show_right_margin#active; - current.show_progress_bar <- show_progress_bar#active; - current.spaces_instead_of_tabs <- spaces_instead_of_tabs#active; - current.highlight_current_line <- highlight_current_line#active; - current.nanoPG <- nanoPG#active; - current.auto_complete <- auto_complete#active; -(* current.tab_length <- tab_width#value_as_int; *) - !refresh_editor_hook () + let button text (pref : bool preference) = + let active = pref#get in + let but = GButton.check_button ~label:text ~active ~packing:box#pack () in + ignore (but#connect#toggled (fun () -> pref#set but#active)) in + let () = button "Dynamic word wrap" dynamic_word_wrap in + let () = button "Show line number" show_line_number in + let () = button "Auto indentation" auto_indent in + let () = button "Auto completion" auto_complete in + let () = button "Show spaces" show_spaces in + let () = button "Show right margin" show_right_margin in + let () = button "Show progress bar" show_progress_bar in + let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in + let () = button "Highlight current line" highlight_current_line in + let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in + let callback () = () in custom ~label box callback true in @@ -600,193 +762,98 @@ let configure ?(apply=(fun () -> ())) () = (string_of_int current.window_width) in *) -(* 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) - "Enable global auto revert" current.global_auto_revert - in + let global_auto_revert = pbool "Enable global auto revert" global_auto_revert in let global_auto_revert_delay = string - ~f:(fun s -> current.global_auto_revert_delay <- + ~f:(fun s -> global_auto_revert_delay#set (try int_of_string s with _ -> 10000)) "Global auto revert delay (ms)" - (string_of_int current.global_auto_revert_delay) + (string_of_int global_auto_revert_delay#get) in - let auto_save = - bool - ~f:(fun s -> current.auto_save <- s) - "Enable auto save" current.auto_save - in + let auto_save = pbool "Enable auto save" auto_save in let auto_save_delay = string - ~f:(fun s -> current.auto_save_delay <- + ~f:(fun s -> auto_save_delay#set (try int_of_string s with _ -> 10000)) "Auto save delay (ms)" - (string_of_int current.auto_save_delay) + (string_of_int auto_save_delay#get) in - let stop_before = - bool - ~f:(fun s -> current.stop_before <- s) - "Stop interpreting before the current point" current.stop_before - in + let stop_before = pbool "Stop interpreting before the current point" stop_before in - let reset_on_tab_switch = - bool - ~f:(fun s -> current.reset_on_tab_switch <- s) - "Reset coqtop on tab switch" current.reset_on_tab_switch - in + let reset_on_tab_switch = pbool "Reset coqtop on tab switch" reset_on_tab_switch in - let vertical_tabs = - bool - ~f:(fun s -> current.vertical_tabs <- s; !refresh_tabs_hook ()) - "Vertical tabs" current.vertical_tabs - in + let vertical_tabs = pbool "Vertical tabs" vertical_tabs in - let opposite_tabs = - bool - ~f:(fun s -> current.opposite_tabs <- s; !refresh_tabs_hook ()) - "Tabs on opposite side" current.opposite_tabs - in + let opposite_tabs = pbool "Tabs on opposite side" opposite_tabs in let encodings = combo "File charset encoding " - ~f:(fun s -> current.encoding <- (inputenc_of_string s)) + ~f:(fun s -> encoding#set (inputenc_of_string s)) ~new_allowed: true - ("UTF-8"::"LOCALE":: match current.encoding with + ("UTF-8"::"LOCALE":: match encoding#get with |Emanual s -> [s] |_ -> [] ) - (string_of_inputenc current.encoding) + (string_of_inputenc encoding#get) in let source_style = - let f s = - current.source_style <- s; - !refresh_style_hook () - in combo "Highlighting style:" - ~f ~new_allowed:false - style_manager#style_scheme_ids current.source_style + ~f:source_style#set ~new_allowed:false + style_manager#style_scheme_ids source_style#get in let source_language = - let f s = - current.source_language <- s; - !refresh_language_hook () - in combo "Language:" - ~f ~new_allowed:false + ~f:source_language#set ~new_allowed:false (List.filter (fun x -> Str.string_match (Str.regexp "^coq") x 0) lang_manager#language_ids) - current.source_language + source_language#get in let read_project = combo "Project file options are" - ~f:(fun s -> current.read_project <- project_behavior_of_string s) + ~f:(fun s -> read_project#set (project_behavior_of_string s)) ~editable:false [string_of_project_behavior Subst_args; string_of_project_behavior Append_args; string_of_project_behavior Ignore_args] - (string_of_project_behavior current.read_project) - in - let project_file_name = - string "Default name for project file" - ~f:(fun s -> current.project_file_name <- s) - current.project_file_name - in - let update_modifiers prefix mds = - let change ~path ~key ~modi ~changed = - if CString.is_sub prefix path 0 then - ignore (GtkData.AccelMap.change_entry ~key ~modi:mds ~replace:true path) - in - GtkData.AccelMap.foreach change + (string_of_project_behavior read_project#get) in - let help_string = - "restart to apply" - in - let the_valid_mod = str_to_mod_list current.modifiers_valid in + let project_file_name = pstring "Default name for project file" project_file_name in let modifier_for_tactics = - let cb l = - current.modifier_for_tactics <- mod_list_to_str l; - update_modifiers "<Actions>/Tactics/" l - in - modifiers - ~allow:the_valid_mod - ~f:cb - ~help:help_string - "Modifiers for Tactics Menu" - (str_to_mod_list current.modifier_for_tactics) + pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics in let modifier_for_templates = - let cb l = - current.modifier_for_templates <- mod_list_to_str l; - update_modifiers "<Actions>/Templates/" l - in - modifiers - ~allow:the_valid_mod - ~f:cb - ~help:help_string - "Modifiers for Templates Menu" - (str_to_mod_list current.modifier_for_templates) + pmodifiers "Modifiers for Templates Menu" modifier_for_templates in let modifier_for_navigation = - let cb l = - current.modifier_for_navigation <- mod_list_to_str l; - update_modifiers "<Actions>/Navigation/" l - in - modifiers - ~allow:the_valid_mod - ~f:cb - ~help:help_string - "Modifiers for Navigation Menu" - (str_to_mod_list current.modifier_for_navigation) + pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation in let modifier_for_display = - let cb l = - current.modifier_for_display <- mod_list_to_str l; - update_modifiers "<Actions>/View/" l - in - modifiers - ~allow:the_valid_mod - ~f:cb - ~help:help_string - "Modifiers for View Menu" - (str_to_mod_list current.modifier_for_display) + pmodifiers "Modifiers for View Menu" modifier_for_display in let modifiers_valid = - modifiers - ~f:(fun l -> - current.modifiers_valid <- mod_list_to_str l) - "Allowed modifiers" - the_valid_mod + pmodifiers ~all:true "Allowed modifiers" modifiers_valid in let cmd_editor = let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in combo ~help:"(%s for file name)" "External editor" - ~f:(fun s -> current.cmd_editor <- s) + ~f:cmd_editor#set ~new_allowed: true - (predefined@[if List.mem current.cmd_editor predefined then "" - else current.cmd_editor]) - current.cmd_editor + (predefined@[if List.mem cmd_editor#get predefined then "" + else cmd_editor#get]) + cmd_editor#get in let cmd_browse = let predefined = [ @@ -799,11 +866,11 @@ let configure ?(apply=(fun () -> ())) () = combo ~help:"(%s for url)" "Browser" - ~f:(fun s -> current.cmd_browse <- s) + ~f:cmd_browse#set ~new_allowed: true - (predefined@[if List.mem current.cmd_browse predefined then "" - else current.cmd_browse]) - current.cmd_browse + (predefined@[if List.mem cmd_browse#get predefined then "" + else cmd_browse#get]) + cmd_browse#get in let doc_url = let predefined = [ @@ -813,11 +880,11 @@ let configure ?(apply=(fun () -> ())) () = ] in combo "Manual URL" - ~f:(fun s -> current.doc_url <- s) + ~f:doc_url#set ~new_allowed: true - (predefined@[if List.mem current.doc_url predefined then "" - else current.doc_url]) - current.doc_url in + (predefined@[if List.mem doc_url#get predefined then "" + else doc_url#get]) + doc_url#get in let library_url = let predefined = [ "file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]); @@ -825,28 +892,22 @@ let configure ?(apply=(fun () -> ())) () = ] in combo "Library URL" - ~f:(fun s -> current.library_url <- s) + ~f:(fun s -> library_url#set s) ~new_allowed: true - (predefined@[if List.mem current.library_url predefined then "" - else current.library_url]) - current.library_url + (predefined@[if List.mem library_url#get predefined then "" + else library_url#get]) + library_url#get in let automatic_tactics = strings - ~f:(fun l -> current.automatic_tactics <- l) + ~f:automatic_tactics#set ~add:(fun () -> ["<edit me>"]) "Wizard tactics to try in order" - current.automatic_tactics + automatic_tactics#get in - let contextual_menus_on_goal = - bool - ~f:(fun s -> - current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal_hook s) - "Contextual menus on goal" current.contextual_menus_on_goal - in + let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch; vertical_tabs;opposite_tabs] in @@ -858,6 +919,8 @@ let configure ?(apply=(fun () -> ())) () = [config_font]); Section("Colors", Some `SELECT_COLOR, [config_color; source_language; source_style]); + Section("Tags", Some `SELECT_COLOR, + [config_tags]); Section("Editor", Some `EDIT, [config_editor]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; diff --git a/ide/preferences.mli b/ide/preferences.mli index 1e4f152c2..b5c7ea222 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -12,95 +12,96 @@ 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 pref = - { - mutable cmd_coqtop : string option; - mutable cmd_coqc : string; - mutable cmd_make : string; - mutable cmd_coqmakefile : string; - mutable cmd_coqdoc : string; - - mutable source_language : string; - mutable source_style : string; - - mutable global_auto_revert : bool; - mutable global_auto_revert_delay : int; - - mutable auto_save : bool; - mutable auto_save_delay : int; - mutable auto_save_name : string * string; - - mutable read_project : project_behavior; - mutable project_file_name : string; - mutable project_path : string option; - - mutable encoding : inputenc; - - mutable automatic_tactics : string list; - mutable cmd_print : string; - - mutable modifier_for_navigation : string; - mutable modifier_for_templates : string; - mutable modifier_for_tactics : string; - mutable modifier_for_display : string; - mutable modifiers_valid : string; - - mutable cmd_browse : string; - mutable cmd_editor : string; - - mutable text_font : Pango.font_description; - - mutable doc_url : string; - mutable library_url : string; - - mutable show_toolbar : bool; - mutable contextual_menus_on_goal : bool; - mutable window_width : int; - mutable window_height : int; - mutable query_window_width : int; - mutable query_window_height : int; -(* - mutable use_utf8_notation : bool; -*) - mutable auto_complete : bool; - mutable stop_before : bool; - mutable reset_on_tab_switch : bool; - mutable vertical_tabs : bool; - mutable opposite_tabs : bool; - - mutable background_color : string; - mutable processing_color : string; - mutable processed_color : string; - mutable error_color : string; - mutable error_fg_color : string; - - mutable dynamic_word_wrap : bool; - mutable show_line_number : bool; - mutable auto_indent : bool; - mutable show_spaces : bool; - mutable show_right_margin : bool; - mutable show_progress_bar : bool; - mutable spaces_instead_of_tabs : bool; - mutable tab_length : int; - mutable highlight_current_line : bool; - - mutable nanoPG : bool; - - } +type tag = { + tag_fg_color : string option; + tag_bg_color : string option; + tag_bold : bool; + tag_italic : bool; + tag_underline : bool; +} + +class type ['a] repr = +object + method into : string list -> 'a option + method from : 'a -> string list +end + +class ['a] preference_signals : changed:'a GUtil.signal -> +object + inherit GUtil.ml_signals + method changed : callback:('a -> unit) -> GtkSignal.id +end + +class ['a] preference : name:string list -> init:'a -> repr:'a repr -> +object + method connect : 'a preference_signals + method get : 'a + method set : 'a -> unit + method reset : unit -> unit + method default : 'a +end + +val list_tags : unit -> tag preference Util.String.Map.t + +val cmd_coqtop : string option preference +val cmd_coqc : string preference +val cmd_make : string preference +val cmd_coqmakefile : string preference +val cmd_coqdoc : string preference +val source_language : string preference +val source_style : string preference +val global_auto_revert : bool preference +val global_auto_revert_delay : int preference +val auto_save : bool preference +val auto_save_delay : int preference +val auto_save_name : (string * string) preference +val read_project : project_behavior preference +val project_file_name : string preference +val project_path : string option preference +val encoding : inputenc preference +val automatic_tactics : string list preference +val cmd_print : string preference +val modifier_for_navigation : string preference +val modifier_for_templates : string preference +val modifier_for_tactics : string preference +val modifier_for_display : string preference +val modifiers_valid : string preference +val cmd_browse : string preference +val cmd_editor : string preference +val text_font : string preference +val doc_url : string preference +val library_url : string preference +val show_toolbar : bool preference +val contextual_menus_on_goal : bool preference +val window_width : int preference +val window_height : int preference +val auto_complete : bool preference +val stop_before : bool preference +val reset_on_tab_switch : bool preference +val vertical_tabs : bool preference +val opposite_tabs : bool preference +val background_color : string preference +val processing_color : string preference +val processed_color : string preference +val error_color : string preference +val error_fg_color : string preference +val dynamic_word_wrap : bool preference +val show_line_number : bool preference +val auto_indent : bool preference +val show_spaces : bool preference +val show_right_margin : bool preference +val show_progress_bar : bool preference +val spaces_instead_of_tabs : bool preference +val tab_length : int preference +val highlight_current_line : bool preference +val nanoPG : bool preference val save_pref : unit -> unit val load_pref : unit -> unit -val current : pref - val configure : ?apply:(unit -> unit) -> unit -> unit -(* Hooks *) -val refresh_editor_hook : (unit -> unit) ref -val refresh_style_hook : (unit -> unit) ref -val refresh_language_hook : (unit -> unit) ref -val refresh_toolbar_hook : (unit -> unit) ref -val resize_window_hook : (unit -> unit) ref -val refresh_tabs_hook : (unit -> unit) ref +val stick : 'a preference -> + (#GObj.widget as 'obj) -> ('a -> unit) -> unit val use_default_doc_url : string diff --git a/ide/session.ml b/ide/session.ml index a795f6331..e4cc17742 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -8,8 +8,6 @@ open Preferences -let prefs = Preferences.current - (** A session is a script buffer + proof + messages, interacting with a coqtop, and a few other elements around *) @@ -18,7 +16,6 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit - method refresh_color : unit -> unit end class type control = @@ -50,8 +47,8 @@ let create_buffer () = let buffer = GSourceView2.source_buffer ~tag_table:Tags.Script.table ~highlight_matching_brackets:true - ?language:(lang_manager#language prefs.source_language) - ?style_scheme:(style_manager#style_scheme prefs.source_style) + ?language:(lang_manager#language source_language#get) + ?style_scheme:(style_manager#style_scheme source_style#get) () in let _ = buffer#create_mark ~name:"start_of_input" buffer#start_iter in @@ -254,10 +251,9 @@ let make_table_widget ?sort cd cb = ~model:store ~packing:frame#add () in let () = data#set_headers_visible true in let () = data#set_headers_clickable true in - let refresh () = - let clr = Tags.color_of_string current.background_color in - data#misc#modify_base [`NORMAL, `COLOR clr] - in + let refresh clr = data#misc#modify_base [`NORMAL, `NAME clr] in + let _ = background_color#connect#changed refresh in + let _ = data#misc#connect#realize (fun () -> refresh background_color#get) in let mk_rend c = GTree.cell_renderer_text [], ["text",c] in let cols = List.map2 (fun (_,c) (_,n,v) -> @@ -285,10 +281,10 @@ let make_table_widget ?sort cd cb = data#connect#row_activated ~callback:(fun tp vc -> cb columns store tp vc) ); let () = match sort with None -> () | Some (i, t) -> store#set_sort_column_id i t in - frame, (fun f -> f columns store), refresh + frame, (fun f -> f columns store) let create_errpage (script : Wg_ScriptView.script_view) : errpage = - let table, access, refresh = + let table, access = make_table_widget ~sort:(0, `ASCENDING) [`Int,"Line",true; `String,"Error message",true] (fun columns store tp vc -> @@ -320,11 +316,10 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = errs end method on_update ~callback:cb = callback := cb - method refresh_color () = refresh () end let create_jobpage coqtop coqops : jobpage = - let table, access, refresh = + let table, access = make_table_widget ~sort:(0, `ASCENDING) [`String,"Worker",true; `String,"Job name",true] (fun columns store tp vc -> @@ -360,7 +355,6 @@ let create_jobpage coqtop coqops : jobpage = jobs end method on_update ~callback:cb = callback := cb - method refresh_color () = refresh () end let create_proof () = diff --git a/ide/session.mli b/ide/session.mli index 52e557218..3a6b45858 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -14,7 +14,6 @@ class type ['a] page = inherit GObj.widget method update : 'a -> unit method on_update : callback:('a -> unit) -> unit - method refresh_color : unit -> unit end class type control = diff --git a/ide/tags.ml b/ide/tags.ml index c9b57af4c..09b562530 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -13,28 +13,15 @@ let make_tag (tt:GText.tag_table) ~name prop = tt#add new_tag#as_tag; new_tag -(* These work fine for colorblind people too *) -let default_processed_color = "light green" -let default_processing_color = "light blue" -let default_error_color = "#FFCCCC" -let default_error_fg_color = "red" -let default_color = "cornsilk" - -let processed_color = ref default_processed_color -let processing_color = ref default_processing_color -let error_color = ref default_error_color -let error_fg_color = ref default_error_fg_color - module Script = struct let table = GText.tag_table () let comment = make_tag table ~name:"comment" [] - let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE ; `FOREGROUND !error_fg_color] - let error_bg = make_tag table ~name:"error_bg" [`BACKGROUND !error_color] - let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color] - let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color] + let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE] + 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" [] let incomplete = make_tag table ~name:"incomplete" [ - `BACKGROUND !processing_color; `BACKGROUND_STIPPLE_SET true; ] let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"] @@ -56,7 +43,7 @@ end module Proof = struct let table = GText.tag_table () - let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color] + let highlight = make_tag table ~name:"highlight" [] let hypothesis = make_tag table ~name:"hypothesis" [] let goal = make_tag table ~name:"goal" [] end @@ -77,34 +64,3 @@ let string_of_color clr = let color_of_string s = let colormap = Gdk.Color.get_system_colormap () in Gdk.Color.alloc ~colormap (`NAME s) - -let get_processed_color () = color_of_string !processed_color - -let set_processed_color clr = - let s = string_of_color clr in - processed_color := s; - Script.processed#set_property (`BACKGROUND s); - Proof.highlight#set_property (`BACKGROUND s) - -let get_processing_color () = color_of_string !processing_color - -let set_processing_color clr = - let s = string_of_color clr in - processing_color := s; - Script.incomplete#set_property (`BACKGROUND s); - Script.to_process#set_property (`BACKGROUND s) - -let get_error_color () = color_of_string !error_color - -let set_error_color clr = - let s = string_of_color clr in - error_color := s; - Script.error_bg#set_property (`BACKGROUND s) - -let get_error_fg_color () = color_of_string !error_fg_color - -let set_error_fg_color clr = - let s = string_of_color clr in - error_fg_color := s; - Script.error#set_property (`FOREGROUND s) - diff --git a/ide/tags.mli b/ide/tags.mli index 14cfd0dbf..6418d1b2e 100644 --- a/ide/tags.mli +++ b/ide/tags.mli @@ -41,22 +41,3 @@ end val string_of_color : Gdk.color -> string val color_of_string : string -> Gdk.color - -val get_processed_color : unit -> Gdk.color -val set_processed_color : Gdk.color -> unit - -val get_processing_color : unit -> Gdk.color -val set_processing_color : Gdk.color -> unit - -val get_error_color : unit -> Gdk.color -val set_error_color : Gdk.color -> unit - -val get_error_fg_color : unit -> Gdk.color -val set_error_fg_color : Gdk.color -> unit - -val default_processed_color : string -val default_processing_color : string -val default_error_color : string -val default_error_fg_color : string -val default_color : string - diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 7dad92ed6..7d8993aa8 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -85,9 +85,11 @@ object(self) ~packing:(vbox#pack ~fill:true ~expand:true) () in let result = GText.view ~packing:r_bin#add () in views <- (frame#coerce, result, combo#entry) :: views; - result#misc#modify_font current.text_font; - let clr = Tags.color_of_string current.background_color in - result#misc#modify_base [`NORMAL, `COLOR clr]; + let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in + let _ = background_color#connect#changed cb in + let _ = result#misc#connect#realize (fun () -> cb background_color#get) in + let cb ft = result#misc#modify_font (Pango.Font.from_string ft) in + stick text_font result cb; result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; let callback () = @@ -98,11 +100,14 @@ object(self) if Str.string_match (Str.regexp "\\. *$") com 0 then com else com ^ " " ^ arg ^" . " in - let log level message = result#buffer#insert (message^"\n") in + let log level message = + Ideutils.insert_xml result#buffer message; + result#buffer#insert "\n"; + in let process = Coq.bind (Coq.query ~logger:log (phrase,Stateid.dummy)) (function | Interface.Fail (_,l,str) -> - result#buffer#insert str; + Ideutils.insert_xml result#buffer str; notebook#set_page ~tab_label:(new_tab_lbl "Error") frame#coerce; Coq.return () | Interface.Good res -> @@ -144,13 +149,9 @@ object(self) method visible = frame#visible - - method refresh_font () = - let iter (_,view,_) = view#misc#modify_font current.text_font in - List.iter iter views - method refresh_color () = - let clr = Tags.color_of_string current.background_color in + method private refresh_color clr = + let clr = Tags.color_of_string clr in let iter (_,view,_) = view#misc#modify_base [`NORMAL, `COLOR clr] in List.iter iter views @@ -158,6 +159,8 @@ object(self) self#new_page_maker; self#new_query_aux ~grab_now:false (); frame#misc#hide (); + let _ = background_color#connect#changed self#refresh_color in + self#refresh_color background_color#get; ignore(notebook#event#connect#key_press ~callback:(fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then (self#hide; true) else false diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli index 91a8f26ca..1f0e31988 100644 --- a/ide/wg_Command.mli +++ b/ide/wg_Command.mli @@ -10,8 +10,6 @@ class command_window : string -> Coq.coqtop -> object method new_query : ?command:string -> ?term:string -> unit -> unit method pack_in : (GObj.widget -> unit) -> unit - method refresh_font : unit -> unit - method refresh_color : unit -> unit method show : unit method hide : unit method visible : bool diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 3f5ae4bd5..7d77679ce 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -258,7 +258,7 @@ object (self) method private refresh_style () = let (renderer, _) = renderer in - let font = Preferences.current.Preferences.text_font in + let font = Pango.Font.from_string Preferences.text_font#get in renderer#set_properties [`FONT_DESC font; `XPAD 10] method private coordinates pos = diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index 211db537e..615e989de 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -6,11 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Preferences + class type message_view_signals = object inherit GObj.misc_signals inherit GUtil.add_ml_signals - method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id + method pushed : callback:Ideutils.logger -> GtkSignal.id end class message_view_signals_impl obj (pushed : 'a GUtil.signal) : message_view_signals = @@ -26,14 +28,13 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : string -> unit - method set : string -> unit - method push : Pp.message_level -> string -> unit + method add : Richpp.richpp -> unit + method add_string : string -> unit + method set : Richpp.richpp -> unit + method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) - method modify_font : Pango.font_description -> unit - method refresh_color : unit -> unit end let message_view () : message_view = @@ -53,6 +54,12 @@ let message_view () : message_view = let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in let () = view#set_left_margin 2 in + view#misc#show (); + let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in + let _ = background_color#connect#changed cb in + let _ = view#misc#connect#realize (fun () -> cb background_color#get) in + let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in + stick text_font view cb; object (self) inherit GObj.widget box#as_widget @@ -70,23 +77,23 @@ let message_view () : message_view = | Pp.Warning -> [Tags.Message.warning] | _ -> [] in - if msg <> "" then begin - buffer#insert ~tags msg; - buffer#insert ~tags "\n"; + let rec non_empty = function + | Xml_datatype.PCData "" -> false + | Xml_datatype.PCData _ -> true + | 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"; push#call (level, msg) end method add msg = self#push Pp.Notice msg + method add_string s = self#add (Richpp.richpp_of_string s) + method set msg = self#clear; self#add msg method buffer = text_buffer - method modify_font fd = view#misc#modify_font fd - - method refresh_color () = - let open Preferences in - let clr = Tags.color_of_string current.background_color in - view#misc#modify_base [`NORMAL, `COLOR clr] - end diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 23c94f404..388ab259f 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -10,7 +10,7 @@ class type message_view_signals = object inherit GObj.misc_signals inherit GUtil.add_ml_signals - method pushed : callback:(Pp.message_level -> string -> unit) -> GtkSignal.id + method pushed : callback:Ideutils.logger -> GtkSignal.id end class type message_view = @@ -18,14 +18,13 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : string -> unit - method set : string -> unit - method push : Pp.message_level -> string -> unit + method add : Richpp.richpp -> unit + method add_string : string -> unit + method set : Richpp.richpp -> unit + method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) - method modify_font : Pango.font_description -> unit - method refresh_color : unit -> unit end val message_view : unit -> message_view diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml index 69d460b01..148add6e9 100644 --- a/ide/wg_ProofView.ml +++ b/ide/wg_ProofView.ml @@ -7,6 +7,8 @@ (************************************************************************) open Util +open Preferences +open Ideutils class type proof_view = object @@ -82,7 +84,8 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with let () = hook_tag_cb tag hint sel_cb on_hover in [tag], hints in - let () = proof#buffer#insert ~tags (hyp ^ "\n") in + let () = insert_xml ~tags proof#buffer hyp in + proof#buffer#insert "\n"; insert_hyp rem_hints hs in let () = proof#buffer#insert head_str in @@ -95,13 +98,14 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with else [] in proof#buffer#insert (goal_str 1 goals_cnt); - proof#buffer#insert ~tags cur_goal; + insert_xml proof#buffer cur_goal; proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = proof#buffer#insert (goal_str i goals_cnt); - proof#buffer#insert (g ^ "\n") + insert_xml proof#buffer g; + proof#buffer#insert "\n" in let () = Util.List.fold_left_i fold_goal 2 () rem_goals in @@ -115,10 +119,12 @@ let mode_cesar (proof : #GText.view_skel) = function | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ -> proof#buffer#insert " *** Declarative Mode ***\n"; List.iter - (fun hyp -> proof#buffer#insert (hyp^"\n")) + (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n") hyps; proof#buffer#insert "______________________________________\n"; - proof#buffer#insert ("thesis := \n "^cur_goal^"\n"); + proof#buffer#insert "thesis := \n "; + insert_xml proof#buffer cur_goal; + proof#buffer#insert "\n"; ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT)) let rec flatten = function @@ -151,8 +157,8 @@ let display mode (view : #GText.view_skel) goals hints evars = (* The proof is finished, with the exception of given up goals. *) view#buffer#insert "No more subgoals, but there are some goals you gave up:\n\n"; let iter goal = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iter iter given_up_goals; view#buffer#insert "\nYou need to go back and solve them." @@ -160,8 +166,8 @@ let display mode (view : #GText.view_skel) goals hints evars = (* All the goals have been resolved but those on the shelf. *) view#buffer#insert "All the remaining goals are on the shelf:\n\n"; let iter goal = - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iter iter shelved_goals | _, _, _, _ -> @@ -173,8 +179,8 @@ let display mode (view : #GText.view_skel) goals hints evars = view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = let () = view#buffer#insert (goal_str (succ i)) in - let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in - view#buffer#insert msg + insert_xml view#buffer goal.Interface.goal_ccl; + view#buffer#insert "\n" in List.iteri iter bg end @@ -193,6 +199,12 @@ let proof_view () = let () = Gtk_parsing.fix_double_click view in let default_clipboard = GData.clipboard Gdk.Atom.primary in let _ = buffer#add_selection_clipboard default_clipboard in + let cb clr = view#misc#modify_base [`NORMAL, `NAME clr] in + let _ = background_color#connect#changed cb in + let _ = view#misc#connect#realize (fun () -> cb background_color#get) in + let cb ft = view#misc#modify_font (Pango.Font.from_string ft) in + stick text_font view cb; + object inherit GObj.widget view#as_widget val mutable goals = None diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 8298d9954..14cbf92eb 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Preferences + type insert_action = { ins_val : string; ins_off : int; @@ -456,6 +458,33 @@ object (self) if not proceed then GtkSignal.stop_emit () in let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in + (** Plug on preferences *) + let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in + let _ = background_color#connect#changed cb in + let _ = self#misc#connect#realize (fun () -> cb background_color#get) in + + let cb b = self#set_wrap_mode (if b then `WORD else `NONE) in + stick dynamic_word_wrap self cb; + stick show_line_number self self#set_show_line_numbers; + stick auto_indent self self#set_auto_indent; + stick highlight_current_line self self#set_highlight_current_line; + + (* Hack to handle missing binding in lablgtk *) + let cb b = + let flag = if b then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *) else 0 in + let conv = Gobject.({ name = "draw-spaces"; conv = Data.int }) in + Gobject.set conv self#as_widget flag + in + stick show_spaces self cb; + + stick show_right_margin self self#set_show_right_margin; + stick spaces_instead_of_tabs self self#set_insert_spaces_instead_of_tabs; + stick tab_length self self#set_tab_width; + stick auto_complete self self#set_auto_complete; + + let cb ft = self#misc#modify_font (Pango.Font.from_string ft) in + stick text_font self cb; + () end diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index 25a031d6e..2ee288454 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -7,6 +7,7 @@ (************************************************************************) open Util +open Preferences type color = GDraw.color @@ -122,6 +123,8 @@ object (self) true in let _ = eventbox#event#connect#button_press clicked_cb in + let cb show = if show then self#misc#show () else self#misc#hide () in + stick show_progress_bar self cb; (** Initial pixmap *) draw#set_pixmap pixmap diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index d337a911d..7445ce5ca 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20140312" +let protocol_version = "20150913" (** * Interface of calls to Coq by CoqIde *) @@ -90,7 +90,7 @@ let of_value f = function | None -> [] | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in let id = Stateid.to_xml id in - Element ("value", ["val", "fail"] @ loc, [id;PCData msg]) + Element ("value", ["val", "fail"] @ loc, [id; Richpp.of_richpp msg]) let to_value f = function | Element ("value", attrs, l) -> let ans = massoc "val" attrs in @@ -103,8 +103,9 @@ let to_value f = function Some (loc_s, loc_e) with Marshal_error | Failure _ -> None in - let id = Stateid.of_xml (List.hd l) in - let msg = raw_string (List.tl l) in + let (id, msg) = match l with [id; msg] -> (id, msg) | _ -> raise Marshal_error in + let id = Stateid.of_xml id in + let msg = Richpp.to_richpp msg in Fail (id, loc, msg) else raise Marshal_error | _ -> raise Marshal_error @@ -131,14 +132,14 @@ let to_evar = function | _ -> raise Marshal_error let of_goal g = - let hyp = of_list of_string g.goal_hyp in - let ccl = of_string g.goal_ccl in + let hyp = of_list Richpp.of_richpp g.goal_hyp in + let ccl = Richpp.of_richpp g.goal_ccl in let id = of_string g.goal_id in Element ("goal", [], [id; hyp; ccl]) let to_goal = function | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_string hyp in - let ccl = to_string ccl in + let hyp = to_list Richpp.to_richpp hyp in + let ccl = Richpp.to_richpp ccl in let id = to_string id in { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } | _ -> raise Marshal_error @@ -318,10 +319,9 @@ end = struct (List.length lg + List.length rg) pr_focus l in Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals else - let pr_menu s = s in let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ - pr_menu goal ^ "]" in + "[" ^ String.concat "; " (List.map Richpp.raw_print hyps) ^ " |- " ^ + Richpp.raw_print goal ^ "]" in String.concat " " (List.map pr_goal g.fg_goals) let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" let pr_status (s : status) = @@ -672,10 +672,10 @@ let to_call : xml -> unknown call = let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]" + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^Richpp.raw_print str^"]" | Fail (id,Some(i,j),str) -> "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^str^"]" + " ("^string_of_int i^","^string_of_int j^")["^Richpp.raw_print str^"]" let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value call value = match call with | Add _ -> pr_value_gen (print add_rty_t ) (Obj.magic value) @@ -731,7 +731,7 @@ let document to_string_fmt = (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34),"error message")))); + (Fail (Stateid.initial,Some (15,34),Richpp.richpp_of_string "error message")))); document_type_encoding to_string_fmt (* vim: set foldmethod=marker: *) |