From 65b901534649c5f29e245a4960fa66f6e9d9c257 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 17 Feb 2016 18:11:02 +0100 Subject: Fix bug #4574: Anomaly: Uncaught exception Invalid_argument("splay_arity"). The setoid_rewrite tactic was not checking that the relation it was looking for was indeed a relation, i.e. that its type was an arity. --- tactics/rewrite.ml | 13 +++++++++---- test-suite/bugs/closed/4574.v | 8 ++++++++ 2 files changed, 17 insertions(+), 4 deletions(-) create mode 100644 test-suite/bugs/closed/4574.v diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 83742bfbd..b04fb660d 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -446,6 +446,8 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof +let error_no_relation () = error "Cannot find a relation to rewrite." + let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) let t = Reductionops.whd_betaiota evd t in @@ -461,8 +463,11 @@ let rec decompose_app_rel env evd t = | App (f, args) -> let len = Array.length args in let fargs = Array.sub args 0 (Array.length args - 2) in - mkApp (f, fargs), args.(len - 2), args.(len - 1) - | _ -> error "Cannot find a relation to rewrite." + let rel = mkApp (f, fargs) in + let ty = Retyping.get_type_of env evd rel in + let () = if not (Reduction.is_arity env ty) then error_no_relation () in + rel, args.(len - 2), args.(len - 1) + | _ -> error_no_relation () let decompose_applied_relation env sigma (c,l) = let ctype = Retyping.get_type_of env sigma c in @@ -2048,8 +2053,8 @@ let setoid_proof ty fn fallback = begin try let rel, _, _ = decompose_app_rel env sigma concl in - let evm = sigma in - let car = pi3 (List.hd (fst (Reduction.dest_prod env (Typing.unsafe_type_of env evm rel)))) in + let (sigma, t) = Typing.type_of env sigma rel in + let car = pi3 (List.hd (fst (Reduction.dest_prod env t))) in (try init_setoid () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e diff --git a/test-suite/bugs/closed/4574.v b/test-suite/bugs/closed/4574.v new file mode 100644 index 000000000..39ba19036 --- /dev/null +++ b/test-suite/bugs/closed/4574.v @@ -0,0 +1,8 @@ +Require Import Setoid. + +Definition block A (a : A) := a. + +Goal forall A (a : A), block Type nat. +Proof. +Fail reflexivity. + -- cgit v1.2.3 From 8a179389fe5199e79d05b2c72ff2aae2061820aa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 17 Feb 2016 18:53:45 +0100 Subject: Fixing the Proofview.Goal.goal function. The environment put in the goals was not the right one and could lead to various leaks. --- proofs/proofview.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 49228c93a..6d7dcb925 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -1000,7 +1000,6 @@ module Goal = struct end let goals = - Env.get >>= fun env -> Pv.get >>= fun step -> let sigma = step.solution in let map goal = @@ -1008,6 +1007,7 @@ module Goal = struct | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = + Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> tclUNIT (gmake env sigma goal) in -- cgit v1.2.3 From 4f640bb24dfc45699670f41441355cdf71c83130 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 15 Feb 2016 16:11:11 +0100 Subject: STM: classify some variants of Instance as regular `Fork nodes. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit "Instance name : Type." is like "Lemma name : Type", i.e. it starts a proof. Unfortunately sometimes it does not, so we say VtUnknown. Still, if there is an open proof, we classify it as a regular Lemma, i.e. the opacity depends only on the terminator. This makes CoqIDE and PIDE based UI way more responsive when processing files containing Instance that are proved by tactics, since they are now correctly delegated to workers. Bug reported privately by Alec Faithfull. --- stm/stm.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/stm/stm.ml b/stm/stm.ml index 56dcda6a4..f2855d508 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2254,7 +2254,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = Proof_global.there_are_pending_proofs () then begin let bname = VCS.mk_branch_name x in - VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[])); + let opacity_of_produced_term = + match x.expr with + | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity + | _ -> Doesn'tGuaranteeOpacity in + VCS.commit id (Fork (x,bname,opacity_of_produced_term,[])); VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1)); Proof_global.activate_proof_mode "Classic"; end else begin -- cgit v1.2.3 From 37479c1b59b7492abb5c89a42c5a76d4cd9d48cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 18 Feb 2016 19:13:40 +0100 Subject: CoqIDE: STOP button also stops workers (fix #4542) --- ide/coq.ml | 15 +++++++++++---- ide/coq.mli | 4 ++-- ide/coqide.ml | 2 +- ide/session.ml | 3 +++ ide/session.mli | 1 + 5 files changed, 18 insertions(+), 7 deletions(-) diff --git a/ide/coq.ml b/ide/coq.ml index 98576a981..7edae47ca 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -465,10 +465,6 @@ let close_coqtop coqtop = let reset_coqtop coqtop = respawn_coqtop ~why:Planned coqtop -let break_coqtop coqtop = - try !interrupter (CoqTop.unixpid coqtop.handle.proc) - with _ -> Minilib.log "Error while sending Ctrl-C" - let get_arguments coqtop = coqtop.sup_args let set_arguments coqtop args = @@ -518,6 +514,17 @@ let search flags = eval_call (Xmlprotocol.search flags) let init x = eval_call (Xmlprotocol.init x) let stop_worker x = eval_call (Xmlprotocol.stop_worker x) +let break_coqtop coqtop workers = + if coqtop.status = Busy then + try !interrupter (CoqTop.unixpid coqtop.handle.proc) + with _ -> Minilib.log "Error while sending Ctrl-C" + else + let rec aux = function + | [] -> Void + | w :: ws -> stop_worker w coqtop.handle (fun _ -> aux ws) + in + let Void = aux workers in () + module PrintOpt = struct type t = string list diff --git a/ide/coq.mli b/ide/coq.mli index d9eda0f34..7cef6a4d0 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -70,8 +70,8 @@ val init_coqtop : coqtop -> unit task -> unit (** Finish initializing a freshly spawned coqtop, by running a first task on it. The task should run its inner continuation at the end. *) -val break_coqtop : coqtop -> unit -(** Interrupt the current computation of coqtop. *) +val break_coqtop : coqtop -> string list -> unit +(** Interrupt the current computation of coqtop or the worker if coqtop it not running. *) val close_coqtop : coqtop -> unit (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *) diff --git a/ide/coqide.ml b/ide/coqide.ml index 608cf82ff..36aab30e6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -574,7 +574,7 @@ module Nav = struct let restart _ = on_current_term restart let interrupt sn = Minilib.log "User break received"; - Coq.break_coqtop sn.coqtop + Coq.break_coqtop sn.coqtop CString.(Set.elements (Map.domain sn.jobpage#data)) let interrupt = cb_on_current_term interrupt let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document) end diff --git a/ide/session.ml b/ide/session.ml index 34c533b8e..168ddd4df 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -19,6 +19,7 @@ class type ['a] page = method update : 'a -> unit method on_update : callback:('a -> unit) -> unit method refresh_color : unit -> unit + method data : 'a end class type control = @@ -321,6 +322,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage = end method on_update ~callback:cb = callback := cb method refresh_color () = refresh () + method data = !last_update end let create_jobpage coqtop coqops : jobpage = @@ -361,6 +363,7 @@ let create_jobpage coqtop coqops : jobpage = end method on_update ~callback:cb = callback := cb method refresh_color () = refresh () + method data = !last_update end let create_proof () = diff --git a/ide/session.mli b/ide/session.mli index 0881e4039..ef39ab2e0 100644 --- a/ide/session.mli +++ b/ide/session.mli @@ -15,6 +15,7 @@ class type ['a] page = method update : 'a -> unit method on_update : callback:('a -> unit) -> unit method refresh_color : unit -> unit + method data : 'a end class type control = -- cgit v1.2.3 From 9aa2d99fb1ad6b348142fce244f277b9dd25017f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Feb 2016 11:51:04 +0100 Subject: STM: Print/Extraction have to be skipped if -quick Print and Extraction commands may pierce opacity: if the task producing the proof term is not finished, we wait for its completion. In -quick mode no worker is going to process a task, since tasks are simply stored to disk (and resumed later in -vio2vo mode). This commit avoids coqc waits forever for a task in order to Print/Extract the corresponding term. Bug reported privately by Alec Faithfull. --- stm/stm.ml | 31 +++++++++++++++++++++++-------- test-suite/vio/print.v | 10 ++++++++++ 2 files changed, 33 insertions(+), 8 deletions(-) create mode 100644 test-suite/vio/print.v diff --git a/stm/stm.ml b/stm/stm.ml index f2855d508..a6d119f0c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -83,6 +83,18 @@ let async_proofs_workers_extra_env = ref [||] type ast = { verbose : bool; loc : Loc.t; mutable expr : vernac_expr } let pr_ast { expr } = pr_vernac expr +(* Commands piercing opaque *) +let may_pierce_opaque = function + | { expr = VernacPrint (PrintName _) } -> true + | { expr = VernacExtend (("Extraction",_), _) } -> true + | { expr = VernacExtend (("SeparateExtraction",_), _) } -> true + | { expr = VernacExtend (("ExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("RecursiveExtractionLibrary",_), _) } -> true + | { expr = VernacExtend (("ExtractionConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInlinedConstant",_), _) } -> true + | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true + | _ -> false + (* Wrapper for Vernacentries.interp to set the feedback id *) let vernac_interp ?proof id ?route { verbose; loc; expr } = let rec internal_command = function @@ -145,7 +157,7 @@ type cmd_t = { ceff : bool; (* is a side-effecting command *) cast : ast; cids : Id.t list; - cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch ] } + cqueue : [ `MainQueue | `TacQueue of cancel_switch | `QueryQueue of cancel_switch | `SkipQueue ] } type fork_t = ast * Vcs_.Branch.t * Vernacexpr.opacity_guarantee * Id.t list type qed_t = { qast : ast; @@ -1665,7 +1677,7 @@ let delegate name = let time = get_hint_bp_time name in time >= 1.0 || !Flags.compilation_mode = Flags.BuildVio || !Flags.async_proofs_full - + let collect_proof keep cur hd brkind id = prerr_endline ("Collecting proof ending at "^Stateid.to_string id); let no_name = "" in @@ -1687,23 +1699,20 @@ let collect_proof keep cur hd brkind id = let has_proof_no_using = function | Some (_, { expr = VernacProof(_,None) }) -> true | _ -> false in - let may_pierce_opaque = function - | { expr = VernacPrint (PrintName _) } -> true - (* These do not exactly pierce opaque, but are anyway impossible to properly - * delegate *) + let too_complex_to_delegate = function | { expr = (VernacDeclareModule _ | VernacDefineModule _ | VernacDeclareModuleType _ | VernacInclude _) } -> true | { expr = (VernacRequire _ | VernacImport _) } -> true - | _ -> false in + | ast -> may_pierce_opaque ast in let parent = function Some (p, _) -> p | None -> assert false in let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in let rec collect last accn id = let view = VCS.visit id in match view.step with | (`Sideff (`Ast(x,_)) | `Cmd { cast = x }) - when may_pierce_opaque x -> `Sync(no_name,None,`Print) + when too_complex_to_delegate x -> `Sync(no_name,None,`Print) | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next | `Sideff (`Ast(x,_)) -> collect (Some (id,x)) (id::accn) view.next (* An Alias could jump everywhere... we hope we can ignore it*) @@ -1811,6 +1820,8 @@ let known_state ?(redefine_qed=false) ~cache id = | `Alias (id,_) -> (fun () -> reach view.next; reach id ), cache, true + | `Cmd { cast = x; cqueue = `SkipQueue } -> (fun () -> + reach view.next), cache, true | `Cmd { cast = x; cqueue = `TacQueue cancel } -> (fun () -> reach ~cache:`Shallow view.next; Hooks.(call tactic_being_run true); @@ -2176,6 +2187,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = let id = VCS.new_node ~id:newtip () in let queue = if !Flags.async_proofs_full then `QueryQueue (ref false) + else if Flags.(!compilation_mode = BuildVio) && + VCS.((get_branch head).kind = `Master) && + may_pierce_opaque x + then `SkipQueue else `MainQueue in VCS.commit id (Cmd {ctac=false;ceff=false;cast = x; cids = []; cqueue = queue }); Backtrack.record (); if w == VtNow then finish (); `Ok diff --git a/test-suite/vio/print.v b/test-suite/vio/print.v new file mode 100644 index 000000000..9c36a463c --- /dev/null +++ b/test-suite/vio/print.v @@ -0,0 +1,10 @@ +Lemma a : True. +Proof. +idtac. +exact I. +Qed. + +Print a. + +Lemma b : False. +Admitted. -- cgit v1.2.3 From d3012c8ac308b18272ddaa90c4eae7e517b63c7c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Feb 2016 13:59:33 +0100 Subject: Fixing bug #4582: cannot override notation [ x ]. --- test-suite/bugs/closed/4582.v | 10 ++++++++++ theories/Lists/List.v | 2 +- 2 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4582.v diff --git a/test-suite/bugs/closed/4582.v b/test-suite/bugs/closed/4582.v new file mode 100644 index 000000000..0842fb8fa --- /dev/null +++ b/test-suite/bugs/closed/4582.v @@ -0,0 +1,10 @@ +Require List. +Import List.ListNotations. + +Variable Foo : nat -> nat. + +Delimit Scope Foo_scope with F. + +Notation " [ x ] " := (Foo x) : Foo_scope. + +Check ([1] : nat)%F. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index cc7586fec..957f1066d 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -26,7 +26,7 @@ In a special module to avoid conflicts. *) Module ListNotations. Notation " [ ] " := nil (format "[ ]") : list_scope. Notation " [ x ] " := (cons x nil) : list_scope. -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +Notation " [ x ; y ; .. ; z ] " := (cons x (cons y .. (cons z nil) ..)) : list_scope. End ListNotations. Import ListNotations. -- cgit v1.2.3 From 924d2833644735a9fa8289ffaa9bac9fbc43982c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 19 Feb 2016 14:27:31 +0100 Subject: Fixing bug #4580: [Set Refine Instance Mode] also used for Program Instance. --- test-suite/bugs/closed/4580.v | 6 ++++++ toplevel/classes.ml | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4580.v diff --git a/test-suite/bugs/closed/4580.v b/test-suite/bugs/closed/4580.v new file mode 100644 index 000000000..4ffd5f0f4 --- /dev/null +++ b/test-suite/bugs/closed/4580.v @@ -0,0 +1,6 @@ +Require Import Program. + +Class Foo (A : Type) := foo : A. + +Unset Refine Instance Mode. +Program Instance f1 : Foo nat := S _. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f73dd5a2e..5f73b70a2 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -290,7 +290,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro if not (Evd.has_undefined evm) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id pl poly evm (Option.get term) termtype - else if !refine_instance || Option.is_empty term then begin + else if Flags.is_program_mode () || !refine_instance || Option.is_empty term then begin let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if Flags.is_program_mode () then let hook vis gr _ = -- cgit v1.2.3 From fd8038facfe10abb2c874ca4602b1d2ee0903056 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 9 Feb 2016 17:46:37 +0100 Subject: Fix regression from 8.4 in reflexivity/... reflexivity/symmetry/transitivity only need RelationClasses to be loaded. --- tactics/rewrite.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index b04fb660d..5ca74050a 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -42,6 +42,10 @@ open Libnames let classes_dirpath = Names.DirPath.make (List.map Id.of_string ["Classes";"Coq"]) +let init_relation_classes () = + if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () + else Coqlib.check_required_library ["Coq";"Classes";"RelationClasses"] + let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] @@ -2041,8 +2045,9 @@ let _ = Hook.set Equality.general_setoid_rewrite_clause general_s_rewrite_clause (** [setoid_]{reflexivity,symmetry,transitivity} tactics *) let not_declared env ty rel = - Tacticals.New.tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++ - str ty ++ str" relation. Maybe you need to require the Setoid library") + Tacticals.New.tclFAIL 0 + (str" The relation " ++ Printer.pr_constr_env env Evd.empty rel ++ str" is not a declared " ++ + str ty ++ str" relation. Maybe you need to require the Coq.Classes.RelationClasses library") let setoid_proof ty fn fallback = Proofview.Goal.nf_enter begin fun gl -> @@ -2055,7 +2060,7 @@ let setoid_proof ty fn fallback = let rel, _, _ = decompose_app_rel env sigma concl in let (sigma, t) = Typing.type_of env sigma rel in let car = pi3 (List.hd (fst (Reduction.dest_prod env t))) in - (try init_setoid () with _ -> raise Not_found); + (try init_relation_classes () with _ -> raise Not_found); fn env sigma car rel with e -> Proofview.tclZERO e end -- cgit v1.2.3 From e54d014ce10dea4a74b66e5091d25e4b26bd71fa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 15 Feb 2016 20:17:24 +0100 Subject: Fixing bug #4540: CoqIDE bottom progress bar does not update. --- ide/coqOps.ml | 67 +++++++++++++++++++++++++-------- ide/document.ml | 27 +++++++++----- ide/document.mli | 4 +- ide/wg_Segment.ml | 106 ++++++++++++++++++++--------------------------------- ide/wg_Segment.mli | 14 +++++-- 5 files changed, 119 insertions(+), 99 deletions(-) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 89f4e513e..58f5eda62 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -169,6 +169,55 @@ let flags_to_color f = module Doc = Document +let segment_model (doc : sentence Doc.document) : Wg_Segment.model = +object (self) + + val mutable cbs = [] + + val mutable document_length = 0 + + method length = document_length + + method changed ~callback = cbs <- callback :: cbs + + method fold : 'a. ('a -> Wg_Segment.color -> 'a) -> 'a -> 'a = fun f accu -> + let fold accu _ _ s = + let flags = List.map mem_flag_of_flag s.flags in + f accu (flags_to_color flags) + in + Doc.fold_all doc accu fold + + method private on_changed (i, f) = + let data = (i, flags_to_color f) in + List.iter (fun f -> f (`SET data)) cbs + + method private on_push s ctx = + let after = match ctx with + | None -> [] + | Some (l, _) -> l + in + List.iter (fun s -> set_index s (s.index + 1)) after; + set_index s (document_length - List.length after); + ignore ((SentenceId.connect s)#changed self#on_changed); + document_length <- document_length + 1; + List.iter (fun f -> f `INSERT) cbs + + method private on_pop s ctx = + let () = match ctx with + | None -> () + | Some (l, _) -> List.iter (fun s -> set_index s (s.index - 1)) l + in + set_index s (-1); + document_length <- document_length - 1; + List.iter (fun f -> f `REMOVE) cbs + + initializer + let _ = (Doc.connect doc)#pushed self#on_push in + let _ = (Doc.connect doc)#popped self#on_pop in + () + +end + class coqops (_script:Wg_ScriptView.script_view) (_pv:Wg_ProofView.proof_view) @@ -201,20 +250,8 @@ object(self) script#misc#set_has_tooltip true; ignore(script#misc#connect#query_tooltip ~callback:self#tooltip_callback); feedback_timer.Ideutils.run ~ms:300 ~callback:self#process_feedback; - let on_changed (i, f) = segment#add i (flags_to_color f) in - let on_push s = - set_index s document_length; - ignore ((SentenceId.connect s)#changed on_changed); - document_length <- succ document_length; - segment#set_length document_length; - let flags = List.map mem_flag_of_flag s.flags in - segment#add s.index (flags_to_color flags); - in - let on_pop s = - set_index s (-1); - document_length <- pred document_length; - segment#set_length document_length; - in + let md = segment_model document in + segment#set_model md; let on_click id = let find _ _ s = Int.equal s.index id in let sentence = Doc.find document find in @@ -230,8 +267,6 @@ object(self) script#buffer#place_cursor iter; ignore (script#scroll_to_iter ~use_align:true ~yalign:0. iter) in - let _ = (Doc.connect document)#pushed on_push in - let _ = (Doc.connect document)#popped on_pop in let _ = segment#connect#clicked on_click in () diff --git a/ide/document.ml b/ide/document.ml index 9823e7576..6566ee3f8 100644 --- a/ide/document.ml +++ b/ide/document.ml @@ -16,8 +16,8 @@ type id = Stateid.t class type ['a] signals = object - method popped : callback:('a -> unit) -> unit - method pushed : callback:('a -> unit) -> unit + method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit + method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit end class ['a] signal () = @@ -32,14 +32,14 @@ end type 'a document = { mutable stack : 'a sentence list; mutable context : ('a sentence list * 'a sentence list) option; - pushed_sig : 'a signal; - popped_sig : 'a signal; + pushed_sig : ('a * ('a list * 'a list) option) signal; + popped_sig : ('a * ('a list * 'a list) option) signal; } -let connect d = +let connect d : 'a signals = object - method pushed ~callback = d.pushed_sig#connect callback - method popped ~callback = d.popped_sig#connect callback + method pushed ~callback = d.pushed_sig#connect (fun (x, ctx) -> callback x ctx) + method popped ~callback = d.popped_sig#connect (fun (x, ctx) -> callback x ctx) end let create () = { @@ -49,6 +49,12 @@ let create () = { popped_sig = new signal (); } +let repr_context s = match s.context with +| None -> None +| Some (cl, cr) -> + let map s = s.data in + Some (List.map map cl, List.map map cr) + (* Invariant, only the tip is a allowed to have state_id = None *) let invariant l = l = [] || (List.hd l).state_id <> None @@ -64,12 +70,13 @@ let tip_data = function let push d x = assert(invariant d.stack); d.stack <- { data = x; state_id = None } :: d.stack; - d.pushed_sig#call x + d.pushed_sig#call (x, repr_context d) let pop = function | { stack = [] } -> raise Empty - | { stack = { data }::xs } as s -> s.stack <- xs; s.popped_sig#call data; data - + | { stack = { data }::xs } as s -> + s.stack <- xs; s.popped_sig#call (data, repr_context s); data + let focus d ~cond_top:c_start ~cond_bot:c_stop = assert(invariant d.stack); if d.context <> None then invalid_arg "focus"; diff --git a/ide/document.mli b/ide/document.mli index 0d803ff00..fb96cb6d7 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -108,8 +108,8 @@ val print : class type ['a] signals = object - method popped : callback:('a -> unit) -> unit - method pushed : callback:('a -> unit) -> unit + method popped : callback:('a -> ('a list * 'a list) option -> unit) -> unit + method pushed : callback:('a -> ('a list * 'a list) option -> unit) -> unit end val connect : 'a document -> 'a signals diff --git a/ide/wg_Segment.ml b/ide/wg_Segment.ml index b4b02a7fa..47fdeb127 100644 --- a/ide/wg_Segment.ml +++ b/ide/wg_Segment.ml @@ -10,53 +10,13 @@ open Util type color = GDraw.color -module Segment : -sig - type +'a t - val length : 'a t -> int - val resize : 'a t -> int -> 'a t - val empty : 'a t - val add : int -> 'a -> 'a t -> 'a t - val remove : int -> 'a t -> 'a t - val fold : ('a -> 'a -> bool) -> (int -> int -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b -end = -struct - type 'a t = { - length : int; - content : 'a Int.Map.t; - } - - let empty = { length = 0; content = Int.Map.empty } - - let length s = s.length - - let resize s len = - if s.length <= len then { s with length = len } - else - let filter i v = i < len in - { length = len; content = Int.Map.filter filter s.content } - - let add i v s = - if i < s.length then - { s with content = Int.Map.add i v s.content } - else s - - let remove i s = { s with content = Int.Map.remove i s.content } - - let fold eq f s accu = - let make k v (cur, accu) = match cur with - | None -> Some (k, k, v), accu - | Some (i, j, w) -> - if k = j + 1 && eq v w then Some (i, k, w), accu - else Some (k, k, v), (i, j, w) :: accu - in - let p, segments = Int.Map.fold make s.content (None, []) in - let segments = match p with - | None -> segments - | Some p -> p :: segments - in - List.fold_left (fun accu (i, j, v) -> f i j v accu) accu segments +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a end let i2f = float_of_int @@ -95,7 +55,7 @@ object (self) val mutable width = 1 val mutable height = 20 - val mutable data = Segment.empty + val mutable model : model option = None val mutable default : color = `WHITE val mutable pixmap : GDraw.pixmap = GDraw.pixmap ~width:1 ~height:1 () val clicked = new GUtil.signal () @@ -113,10 +73,12 @@ object (self) end in let _ = box#misc#connect#size_allocate cb in - let clicked_cb ev = + let clicked_cb ev = match model with + | None -> true + | Some md -> let x = GdkEvent.Button.x ev in let (width, _) = pixmap#size in - let len = Segment.length data in + let len = md#length in let idx = f2i ((x *. i2f len) /. i2f width) in let () = clicked#call idx in true @@ -125,17 +87,23 @@ object (self) (** Initial pixmap *) draw#set_pixmap pixmap - method length = Segment.length data - - method set_length len = - data <- Segment.resize data len; - if self#misc#visible then self#refresh () + method set_model md = + model <- Some md; + let changed_cb = function + | `INSERT | `REMOVE -> + if self#misc#visible then self#refresh () + | `SET (i, color) -> + if self#misc#visible then self#fill_range color i (i + 1) + in + md#changed changed_cb - method private fill_range color i j = + method private fill_range color i j = match model with + | None -> () + | Some md -> let i = i2f i in let j = i2f j in let width = i2f width in - let len = i2f (Segment.length data) in + let len = i2f md#length in let x = f2i ((i *. width) /. len) in let x' = f2i ((j *. width) /. len) in let w = x' - x in @@ -143,14 +111,6 @@ object (self) pixmap#rectangle ~x ~y:0 ~width:w ~height ~filled:true (); draw#set_mask None; - method add i color = - data <- Segment.add i color data; - if self#misc#visible then self#fill_range color i (i + 1) - - method remove i = - data <- Segment.remove i data; - if self#misc#visible then self#fill_range default i (i + 1) - method set_default_color color = default <- color method default_color = default @@ -159,11 +119,23 @@ object (self) draw#set_pixmap pixmap; self#refresh (); - method private refresh () = + method private refresh () = match model with + | None -> () + | Some md -> pixmap#set_foreground default; pixmap#rectangle ~x:0 ~y:0 ~width ~height ~filled:true (); - let fold i j v () = self#fill_range v i (j + 1) in - Segment.fold color_eq fold data (); + let make (k, cur, accu) v = match cur with + | None -> pred k, Some (k, k, v), accu + | Some (i, j, w) -> + if k = j - 1 && color_eq v w then pred k, Some (k, i, w), accu + else pred k, Some (k, k, v), (i, j, w) :: accu + in + let _, p, segments = md#fold make (md#length - 1, None, []) in + let segments = match p with + | None -> segments + | Some p -> p :: segments + in + List.iter (fun (i, j, v) -> self#fill_range v i (j + 1)) segments; draw#set_mask None; method connect = diff --git a/ide/wg_Segment.mli b/ide/wg_Segment.mli index 0fc8ebd75..29cbbedac 100644 --- a/ide/wg_Segment.mli +++ b/ide/wg_Segment.mli @@ -8,6 +8,8 @@ type color = GDraw.color +type model_event = [ `INSERT | `REMOVE | `SET of int * color ] + class type segment_signals = object inherit GObj.misc_signals @@ -15,15 +17,19 @@ object method clicked : callback:(int -> unit) -> GtkSignal.id end +class type model = +object + method changed : callback:(model_event -> unit) -> unit + method length : int + method fold : 'a. ('a -> color -> 'a) -> 'a -> 'a +end + class segment : unit -> object inherit GObj.widget val obj : Gtk.widget Gtk.obj + method set_model : model -> unit method connect : segment_signals - method length : int - method set_length : int -> unit method default_color : color method set_default_color : color -> unit - method add : int -> color -> unit - method remove : int -> unit end -- cgit v1.2.3