diff options
| -rw-r--r-- | ide/coq.ml | 2 | ||||
| -rw-r--r-- | ide/coq.mli | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 89 | ||||
| -rw-r--r-- | ide/ide.mllib | 1 | ||||
| -rw-r--r-- | ide/indent.ml | 148 | ||||
| -rw-r--r-- | ide/indent.mli | 30 | ||||
| -rw-r--r-- | ide/preferences.ml | 85 | ||||
| -rw-r--r-- | ide/preferences.mli | 9 | ||||
| -rw-r--r-- | toplevel/ide_blob.ml | 9 | ||||
| -rw-r--r-- | toplevel/ide_blob.mli | 2 |
10 files changed, 364 insertions, 13 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 227f1fb7e..66fcbd059 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -247,4 +247,6 @@ let goals coqtop = let make_cases coqtop s = eval_call coqtop (Ide_blob.make_cases s) +let contents coqtop = eval_call coqtop (Ide_blob.contents) + let current_status coqtop = eval_call coqtop Ide_blob.current_status diff --git a/ide/coq.mli b/ide/coq.mli index 6bc593477..9c39409ab 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -57,6 +57,8 @@ val is_in_loadpath : coqtop -> string -> bool Ide_blob.value val make_cases : coqtop -> string -> string list list Ide_blob.value +val contents : coqtop -> Lib.library_segment Ide_blob.value + (* Message to display in lower status bar. *) val current_status : coqtop -> string Ide_blob.value diff --git a/ide/coqide.ml b/ide/coqide.ml index 8845cade0..25bbf0ef4 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -31,7 +31,7 @@ object('self) val message_view : GText.view val proof_buffer : GText.buffer val proof_view : GText.view - val cmd_stack : ide_info Stack.t + val cmd_stack : (ide_info * Indent.interp_node) Stack.t val mutable is_active : bool val mutable read_only : bool val mutable filename : string option @@ -67,7 +67,8 @@ object('self) method get_insert : GText.iter method get_start_of_input : GText.iter method go_to_insert : unit - method indent_current_line : unit + method indent_current_line_using_previous_line : unit + method indent_current_line_using_levels : unit method go_to_next_occ_of_cur_word : unit method go_to_prev_occ_of_cur_word : unit method insert_command : string -> string -> unit @@ -539,6 +540,12 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = let sup_args = ref "" +let current_interp_node stk = + try + let (_, pno) = Stack.top stk in + pno + with Stack.Empty -> Indent.first_interp_node + class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct = object(self) val input_view = _script @@ -557,6 +564,7 @@ object(self) val mutable last_auto_save_time = 0. val mutable detached_views = [] val mutable find_forward_instead_of_backward = false + val mutable tab_one_tap = false val mutable auto_complete_on = !current.auto_complete val hidden_proofs = Hashtbl.create 32 @@ -726,7 +734,7 @@ object(self) `INSERT) - method indent_current_line = + method indent_current_line_using_previous_line = let get_nb_space it = let it = it#copy in let nb_sep = ref 0 in @@ -756,6 +764,45 @@ object(self) end + method indent_current_line_using_levels = + let get_nb_space it = + let it = it#copy in + let nb_sep = ref 0 in + let continue = ref true in + while !continue do + if it#char = space then begin + incr nb_sep; + if not it#nocopy#forward_char then continue := false; + end else continue := false + done; + !nb_sep + in + let current_line_start = self#get_insert#set_line_offset 0 in + let current_line_spaces = get_nb_space current_line_start in + if input_buffer#delete_interactive + ~start:current_line_start + ~stop:(current_line_start#forward_chars current_line_spaces) + () + then + let current_line_start = self#get_insert#set_line_offset 0 in + let levels = Indent.compute_nesting (current_interp_node cmd_stack) in + let common_shift = + !current.indent_module_factor * levels.Indent.module_levels + + !current.indent_section_factor * levels.Indent.section_levels + in + let additionnal_shift = + if !current.indent_tactic_was_mode + then !current.indent_was_factor * levels.Indent.tactic_levels + + if levels.Indent.tactic_alinea + then 0 + else !current.indent_was_alinea + else !current.indent_saw_factor * levels.Indent.subgoal_levels + in + let shifting = common_shift + additionnal_shift in + input_buffer#insert + ~iter:current_line_start + (String.make shifting ' ') + method go_to_next_occ_of_cur_word = let cv = session_notebook#current_term in let av = cv.analyzed_view in @@ -926,7 +973,13 @@ object(self) end; let ide_payload = { start = `MARK (b#create_mark start); stop = `MARK (b#create_mark stop); } in - Stack.push ide_payload cmd_stack; + let (interp_node, e_msg_opt) = Indent.compute_interp_node + (Coq.goals mycoqtop) + (current_interp_node cmd_stack) + (Coq.contents mycoqtop) + in + Stack.push (ide_payload, interp_node) cmd_stack; +(* (match e_msg_opt with Some(s) -> flash_info s | _ -> ());*) if display_goals then self#show_goals; remove_tag (start,stop) in begin @@ -954,7 +1007,13 @@ object(self) input_buffer#place_cursor ~where:stop; let ide_payload = { start = `MARK (input_buffer#create_mark start); stop = `MARK (input_buffer#create_mark stop); } in - Stack.push ide_payload cmd_stack; + let (interp_node, e_msg_opt) = Indent.compute_interp_node + (Coq.goals mycoqtop) + (current_interp_node cmd_stack) + (Coq.contents mycoqtop) + in + Stack.push (ide_payload, interp_node) cmd_stack; +(* (match e_msg_opt with Some(s) -> flash_info s | _ -> ());*) self#show_goals; (*Auto insert save on success... try (match Coq.get_current_goals () with @@ -1028,7 +1087,7 @@ object(self) method reset_initial = sync (fun _ -> Stack.iter - (function inf -> + (function (inf, _) -> let start = input_buffer#get_iter_at_mark inf.start in let stop = input_buffer#get_iter_at_mark inf.stop in input_buffer#move_mark ~where:start (`NAME "start_of_input"); @@ -1049,11 +1108,11 @@ object(self) (* pop Coq commands until we reach iterator [i] *) let rec n_step n = if Stack.is_empty cmd_stack then n else - let ide_ri = Stack.pop cmd_stack in + let (ide_ri, ide_ii) = Stack.pop cmd_stack in if i#compare (input_buffer#get_iter_at_mark ide_ri.stop) < 0 then n_step (succ n) else - (Stack.push ide_ri cmd_stack; n) + (Stack.push (ide_ri, ide_ii) cmd_stack; n) in begin try @@ -1065,7 +1124,8 @@ object(self) sync (fun _ -> let start = if Stack.is_empty cmd_stack then input_buffer#start_iter - else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in + else input_buffer#get_iter_at_mark + (fst (Stack.top cmd_stack)).stop in prerr_endline "Removing (long) processed tag..."; input_buffer#remove_tag Tags.Script.processed @@ -1102,7 +1162,7 @@ object(self) if Mutex.try_lock coq_may_stop then (push_info "Undoing last step..."; (try - let ide_ri = Stack.pop cmd_stack in + let (ide_ri, _) = Stack.pop cmd_stack in let start = input_buffer#get_iter_at_mark ide_ri.start in let update_input () = prerr_endline "Removing processed tag..."; @@ -1146,6 +1206,8 @@ object(self) ("progress "^p^".\n") (p^".\n")) l) method active_keypress_handler k = + (if GdkEvent.Key.keyval k <> GdkKeysyms._Tab + then tab_one_tap <- false); let state = GdkEvent.Key.state k in begin match state with @@ -1168,7 +1230,12 @@ object(self) | l -> if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin prerr_endline "active_kp_handler for Tab"; - self#indent_current_line; + begin + tab_one_tap <- not tab_one_tap; + if tab_one_tap + then self#indent_current_line_using_levels + else self#indent_current_line_using_previous_line + end; true end else false end diff --git a/ide/ide.mllib b/ide/ide.mllib index 87b66baba..af9861c3a 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -20,4 +20,5 @@ Undo Coq Coq_commands Command_windows +Indent Coqide diff --git a/ide/indent.ml b/ide/indent.ml new file mode 100644 index 000000000..05afb6f2a --- /dev/null +++ b/ide/indent.ml @@ -0,0 +1,148 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type proof_node = { + (* In saw mode, identation depends directly from + * the remaining subgoals to be proven + * *) + remaining_subgoals : int; + (* A subgoal stack is a list of remaining subgoals + * at each "keypoint"; + * + * Imagine you have to solve a subgoal "S", and you + * know that "n" subgoals remain to be proved. + * + * After running a tactic, let us call "m" the number of + * remaining subgoals to be proven; 3 cases occur: + * - if "m" > "n", then you know that you have entered a + * new indentation level and that you will close it + * once the remaining goals are below "n", so + * we push "n" in this case to keep track of it + * - if "m" = "n" then nothing changes + * - if "m" < "n" then according to the first case we + * have to look if the top of our stack is below "n"; + * if so we pop our stack, so that our indentation + * level is always equal to depth of our stack + * *) + subgoals_stack : int list; + (* [first_step] means that the number of remaining + * subgoals has changed (cases 1 and 3 of previous enumeration) + * *) + first_step : bool; +} +type interp_node = { + opened_sections : int; + opened_modules : int; + interp_mode : proof_node option; +} + +(* In the first step, we have not yet any interp node, + * but we need one to use [compute_interp_node], + * so we provide one + * *) +let first_interp_node = { + opened_sections = 0; + opened_modules = 0; + interp_mode = None; +} + +(* this functions finds how many modules and sections are opened *) +let get_opened lstk = + let rec get_opened lstk (sections, modules) = + match lstk with + | [] -> (sections, modules) + | (_, node)::lstk -> get_opened lstk + ( match node with + | Lib.OpenedModule(_,_,_) + | Lib.OpenedModtype(_,_) -> + sections, 1+modules + | Lib.OpenedSection(_,_) -> + 1+sections, modules +(* | Lib.ClosedModule(_) + | Lib.ClosedModtype(_) -> + sections, modules-1 + | Lib.ClosedSection(_) -> + sections-1, modules*) + | _ -> sections, modules + ) + in + match lstk with + | Ide_blob.Fail(_,_) -> (0,0) + | Ide_blob.Good lstk -> get_opened lstk (0, 0) + +(* given the current pftreestate + * (or None if we are neither in proof nor tactic mode) + * and the previous proof_node, we can compute the + * current proof_node + * *) +let compute_interp_node pftso pno lstk = + let (i_mode, o_msg) = + match pftso with + | Ide_blob.Fail(_,_) -> (None, None) + | Ide_blob.Good (Ide_blob.Message s) -> (None, None) + | Ide_blob.Good (Ide_blob.Goals goals) -> + (* we need the number of remaining subgoals in tactic mode *) + let rs = List.length goals in + (* and the indication that the proof is really terminated in case + * rs = 0 for declarative mode + * *) + if rs = 0 + then (None, None) + else + let (fs, (ss, e_msg)) = + match pno.interp_mode with + | None -> (true, ([], None)) + | Some pn -> + let (fs, (ss, e_msg)) = + if rs = pn.remaining_subgoals + then (false, (pn.subgoals_stack, None)) + else (true, + if rs > pn.remaining_subgoals + then (pn.remaining_subgoals::pn.subgoals_stack, None) + else let rec unhead l = match l with + | [] -> ([], Some("Indentation system broken")) + |h::t-> if h = pn.remaining_subgoals + then unhead t + else (h::t, None) + in unhead pn.subgoals_stack) + in (fs, (ss, e_msg)) + in + (Some { remaining_subgoals = rs; + subgoals_stack = ss; + first_step = fs; + }, + e_msg) + in + let (s, m) = get_opened lstk in + { opened_sections = s; + opened_modules = m; + interp_mode = i_mode; + }, o_msg + +type nesting = { + module_levels : int; (* number of opened modules *) + section_levels : int; (* number of opened sections *) + subgoal_levels : int; (* number of remaining subgoals *) + tactic_levels : int; (* number of imbricated proofs *) + tactic_alinea : bool; (* are we entering a new node? *) +} + +let compute_nesting pno = + let subgoals, tactic_depth, alinea = + match pno.interp_mode with + | None -> (0, 0, true) + | Some pn -> (pn.remaining_subgoals, + List.length pn.subgoals_stack, + pn.first_step) + in + { section_levels = pno.opened_sections; + module_levels = pno.opened_modules; + subgoal_levels = subgoals; + tactic_levels = tactic_depth; + tactic_alinea = alinea; + } diff --git a/ide/indent.mli b/ide/indent.mli new file mode 100644 index 000000000..f57ca1d44 --- /dev/null +++ b/ide/indent.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* some data to have informations on how we can indent proofs *) +type interp_node + +(* the default value of this data *) +val first_interp_node : interp_node + +(* the function to compute our data *) +val compute_interp_node : + Ide_blob.goals Ide_blob.value -> + interp_node -> Lib.library_segment Ide_blob.value -> interp_node * string option + +(* our data are abstract, so we need to get access to some of it informations to + * use it; that is the aim of (compute_nesting) + * *) +type nesting = { + module_levels : int; + section_levels : int; + subgoal_levels : int; + tactic_levels : int; + tactic_alinea : bool; +} +val compute_nesting : interp_node -> nesting diff --git a/ide/preferences.ml b/ide/preferences.ml index a6aaef257..aabedbe7a 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -96,6 +96,15 @@ type pref = mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; +(* + for indentation in proof mode +*) + mutable indent_module_factor : int; + mutable indent_section_factor : int; + mutable indent_saw_factor : int; + mutable indent_was_factor : int; + mutable indent_was_alinea : int; + mutable indent_tactic_was_mode : bool; } let use_default_doc_url = "(automatic)" @@ -152,6 +161,13 @@ let (current:pref ref) = lax_syntax = true; vertical_tabs = false; opposite_tabs = false; + + indent_module_factor = 1; + indent_section_factor = 1; + indent_saw_factor = 1; + indent_was_factor = 3; + indent_was_alinea = 1; + indent_tactic_was_mode = false; } @@ -219,6 +235,14 @@ let save_pref () = add "lax_syntax" [string_of_bool p.lax_syntax] ++ add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ + + add "indent_module_factor" [string_of_int p.indent_module_factor] ++ + add "indent_section_factor" [string_of_int p.indent_section_factor] ++ + add "indent_saw_factor" [string_of_int p.indent_saw_factor] ++ + add "indent_was_factor" [string_of_int p.indent_was_factor] ++ + add "indent_was_alinea" [string_of_int p.indent_was_alinea] ++ + add "indent_tactic_was_mode" + [string_of_bool p.indent_tactic_was_mode] ++ Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." @@ -287,6 +311,13 @@ let load_pref () = set_bool "lax_syntax" (fun v -> np.lax_syntax <- v); set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); + set_int "indent_module_factor" (fun v -> np.indent_module_factor <- v); + set_int "indent_section_factor" (fun v -> np.indent_section_factor <- v); + set_int "indent_saw_factor" (fun v -> np.indent_saw_factor <- v); + set_int "indent_was_factor" (fun v -> np.indent_was_factor <- v); + set_int "indent_was_alinea" (fun v -> np.indent_was_alinea <- v); + set_bool "indent_tactic_was_mode" + (fun v -> np.indent_tactic_was_mode <- v); current := np; (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); @@ -569,6 +600,53 @@ let configure ?(apply=(fun () -> ())) () = "Contextual menus on goal" !current.contextual_menus_on_goal in + let indent_module_factor = + string + ~f:(fun s -> let i = try int_of_string s with _ -> 1 in + !current.indent_module_factor <- i) + "Modules depth dependent shifting for indentation" + (string_of_int !current.indent_module_factor) + in + + let indent_section_factor = + string + ~f:(fun s -> let i = try int_of_string s with _ -> 1 in + !current.indent_section_factor <- i) + "Sections depth dependent shifting for indentation" + (string_of_int !current.indent_section_factor) + in + + let indent_saw_factor = + string + ~f:(fun s -> let i = try int_of_string s with _ -> 1 in + !current.indent_saw_factor <- i) + "Shifting factor in \"saw mode\" (remaining subgoals dependent)" + (string_of_int !current.indent_saw_factor) + in + + let indent_was_factor = + string + ~f:(fun s -> let i = try int_of_string s with _ -> 3 in + !current.indent_was_factor <- i) + "Shifting factor in \"was mode\" (proof depth dependent)" + (string_of_int !current.indent_was_factor) + in + + let indent_was_alinea = + string + ~f:(fun s -> let i = try int_of_string s with _ -> 1 in + !current.indent_was_alinea <- i) + "Constant shift for stagnant subgoals (was mode)" + (string_of_int !current.indent_was_alinea) + in + + let indent_tactic_was_mode = + bool + ~f:(fun s -> !current.indent_tactic_was_mode <- s) + "tactic mode : indentation in \"was mode\" instead of \"saw mode\"" + !current.indent_tactic_was_mode + in + let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; vertical_tabs;opposite_tabs] in @@ -594,7 +672,12 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", [modifiers_valid; modifier_for_tactics; - modifier_for_templates; modifier_for_display; modifier_for_navigation]); + modifier_for_templates; modifier_for_display; + modifier_for_navigation]); + Section("Indentation", + [indent_module_factor; indent_section_factor; + indent_saw_factor; indent_was_factor; indent_was_alinea; + indent_tactic_was_mode]); Section("Misc", misc)] in diff --git a/ide/preferences.mli b/ide/preferences.mli index 41a581d57..723a771b0 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -55,6 +55,15 @@ type pref = mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; +(* + * for indentation + *) + mutable indent_module_factor : int; + mutable indent_section_factor : int; + mutable indent_saw_factor : int; + mutable indent_was_factor : int; + mutable indent_was_alinea : int; + mutable indent_tactic_was_mode : bool; } val save_pref : unit -> unit diff --git a/toplevel/ide_blob.ml b/toplevel/ide_blob.ml index c4036af9f..1fd42e419 100644 --- a/toplevel/ide_blob.ml +++ b/toplevel/ide_blob.ml @@ -512,6 +512,7 @@ let explain_exn e = in toploc,(Cerrors.explain_exn exc) +let contents () = Lib.contents_after None (** * Wrappers around Coq calls. We use phantom types and GADT to protect ourselves @@ -527,6 +528,7 @@ type 'a call = | Cur_goals | Cur_status | Cases of string + | Contents type 'a value = | Good of 'a @@ -546,7 +548,9 @@ let eval_call c = | Read_stdout -> Obj.magic (read_stdout ()) | Cur_goals -> Obj.magic (current_goals ()) | Cur_status -> Obj.magic (current_status ()) - | Cases s -> Obj.magic (make_cases s)) + | Cases s -> Obj.magic (make_cases s) + | Contents -> Obj.magic (contents ()) + ) with e -> let (l,pp) = explain_exn (filter_compat_exn e) in (* force evaluation of format stream *) @@ -576,6 +580,9 @@ let current_status : string call = let make_cases s : string list list call = Cases s +let contents : Lib.library_segment call = + Contents + (* End of wrappers *) let loop () = diff --git a/toplevel/ide_blob.mli b/toplevel/ide_blob.mli index 34879f057..b1261e496 100644 --- a/toplevel/ide_blob.mli +++ b/toplevel/ide_blob.mli @@ -43,4 +43,6 @@ val current_goals : goals call val read_stdout : string call +val contents : Lib.library_segment call + val loop : unit -> unit |