diff options
author | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 12:20:08 +0000 |
---|---|---|
committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-06 12:20:08 +0000 |
commit | c515d65d6ee81f532cb227419bbef36701593aa0 (patch) | |
tree | f483536de38d9be4c3f51f0e062baf8bf2c0dd67 /ide | |
parent | eed2bb82eb4b97881f155079fd457a8de75bdba5 (diff) |
Reverted r13715 "Add improved indenters that rely on the current proof state to choose the indentation depth."
It seems to be the cause for bug #2472.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13766 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-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 |
8 files changed, 12 insertions, 354 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 5db5f0f3a..5c7d8cce8 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -250,6 +250,4 @@ 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 9c39409ab..6bc593477 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -57,8 +57,6 @@ 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 25bbf0ef4..8845cade0 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 * Indent.interp_node) Stack.t + val cmd_stack : ide_info Stack.t val mutable is_active : bool val mutable read_only : bool val mutable filename : string option @@ -67,8 +67,7 @@ object('self) method get_insert : GText.iter method get_start_of_input : GText.iter method go_to_insert : unit - method indent_current_line_using_previous_line : unit - method indent_current_line_using_levels : unit + method indent_current_line : 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 @@ -540,12 +539,6 @@ 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 @@ -564,7 +557,6 @@ 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 @@ -734,7 +726,7 @@ object(self) `INSERT) - method indent_current_line_using_previous_line = + method indent_current_line = let get_nb_space it = let it = it#copy in let nb_sep = ref 0 in @@ -764,45 +756,6 @@ 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 @@ -973,13 +926,7 @@ object(self) end; let ide_payload = { start = `MARK (b#create_mark start); stop = `MARK (b#create_mark stop); } in - 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 | _ -> ());*) + Stack.push ide_payload cmd_stack; if display_goals then self#show_goals; remove_tag (start,stop) in begin @@ -1007,13 +954,7 @@ 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 - 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 | _ -> ());*) + Stack.push ide_payload cmd_stack; self#show_goals; (*Auto insert save on success... try (match Coq.get_current_goals () with @@ -1087,7 +1028,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"); @@ -1108,11 +1049,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, ide_ii) = Stack.pop cmd_stack in + let ide_ri = 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, ide_ii) cmd_stack; n) + (Stack.push ide_ri cmd_stack; n) in begin try @@ -1124,8 +1065,7 @@ object(self) sync (fun _ -> let start = if Stack.is_empty cmd_stack then input_buffer#start_iter - else input_buffer#get_iter_at_mark - (fst (Stack.top cmd_stack)).stop in + else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in prerr_endline "Removing (long) processed tag..."; input_buffer#remove_tag Tags.Script.processed @@ -1162,7 +1102,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..."; @@ -1206,8 +1146,6 @@ 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 @@ -1230,12 +1168,7 @@ object(self) | l -> if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin prerr_endline "active_kp_handler for Tab"; - 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; + self#indent_current_line; true end else false end diff --git a/ide/ide.mllib b/ide/ide.mllib index af9861c3a..87b66baba 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -20,5 +20,4 @@ Undo Coq Coq_commands Command_windows -Indent Coqide diff --git a/ide/indent.ml b/ide/indent.ml deleted file mode 100644 index 05afb6f2a..000000000 --- a/ide/indent.ml +++ /dev/null @@ -1,148 +0,0 @@ -(************************************************************************) -(* 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 deleted file mode 100644 index f57ca1d44..000000000 --- a/ide/indent.mli +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* 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 aabedbe7a..a6aaef257 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -96,15 +96,6 @@ 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)" @@ -161,13 +152,6 @@ 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; } @@ -235,14 +219,6 @@ 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." @@ -311,13 +287,6 @@ 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); @@ -600,53 +569,6 @@ 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 @@ -672,12 +594,7 @@ let configure ?(apply=(fun () -> ())) () = [automatic_tactics]); Section("Shortcuts", [modifiers_valid; modifier_for_tactics; - 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]); + modifier_for_templates; modifier_for_display; modifier_for_navigation]); Section("Misc", misc)] in diff --git a/ide/preferences.mli b/ide/preferences.mli index 723a771b0..41a581d57 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -55,15 +55,6 @@ 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 |