From d6fe6773c959493ed97108e1032b1bd8c1e78081 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 24 Oct 2016 18:18:33 +0200 Subject: Lets Hints/Instances take an optional pattern In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well. --- printing/ppvernac.ml | 22 ++++++++++++++-------- printing/prettyp.ml | 2 +- 2 files changed, 15 insertions(+), 9 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 5455ab891a..3494ad006f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -166,14 +166,17 @@ module Make | ModeNoHeadEvar -> str"!" | ModeOutput -> str"-" + let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } = + pr_opt (fun x -> str"|" ++ int x) pri ++ + pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat + let pr_hints db h pr_c pr_pat = let opth = pr_opt_hintbases db in let pph = match h with | HintsResolve l -> keyword "Resolve " ++ prlist_with_sep sep - (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++ - match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ()) + (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info) l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ @@ -888,7 +891,7 @@ module Make spc() ++ pr_class_rawexpr c2) ) - | VernacInstance (abst, sup, (instid, bk, cl), props, pri) -> + | VernacInstance (abst, sup, (instid, bk, cl), props, info) -> return ( hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ @@ -899,7 +902,7 @@ module Make pr_and_type_binders_arg sup ++ str":" ++ spc () ++ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ - pr_constr cl ++ pr_priority pri ++ + pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with | Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false @@ -913,11 +916,14 @@ module Make keyword "Context" ++ spc () ++ pr_and_type_binders_arg l) ) - | VernacDeclareInstances (ids, pri) -> - return ( + | VernacDeclareInstances insts -> + let pr_inst (id, info) = + pr_reference id ++ pr_hint_info pr_constr_pattern_expr info + in + return ( hov 1 (keyword "Existing" ++ spc () ++ - keyword(String.plural (List.length ids) "Instance") ++ - spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri) + keyword(String.plural (List.length insts) "Instance") ++ + spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts) ) | VernacDeclareClass id -> diff --git a/printing/prettyp.ml b/printing/prettyp.ml index b590a8c930..e117f1dcb0 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -872,7 +872,7 @@ let pr_instance env i = (* gallina_print_constant_with_infos i.is_impl *) (* lighter *) print_ref false (instance_impl i) ++ - begin match instance_priority i with + begin match hint_priority i with | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i end -- cgit v1.2.3 From f558a0552b49b533c1c79ee3eb6d49015eeb6084 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 4 Nov 2016 16:10:31 +0100 Subject: Do not print dependent evars by default (expensive) The option can be turned on by the user though. --- printing/printer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 608bca62ac..04337f6be8 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -529,7 +529,7 @@ let print_evar_constraints gl sigma = str" with candidates:" ++ fnl () ++ hov 0 ppcandidates else mt () -let should_print_dependent_evars = ref true +let should_print_dependent_evars = ref false let _ = let open Goptions in -- cgit v1.2.3 From 26d180fa0b27edc773fd07c73906e4ed56475200 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 16 Nov 2016 10:51:39 +0100 Subject: [stm] Remove STM-related vernaculars I think these commands never make a lot of sense on scripts other than debugging and we have better methods now. The last remaining command, used for the tty emulation has been renamed to VtBack, but it should go away at some point too once the legacy interfaces are removed. --- printing/ppvernac.ml | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3494ad006f..a6b1c97f5c 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -538,22 +538,6 @@ module Make | VernacLocal (local, v) -> return (pr_locality local ++ spc() ++ pr_vernac_body v) - (* Stm *) - | VernacStm JoinDocument -> - return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") - | VernacStm Wait -> - return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) - (* Proof management *) | VernacAbortAll -> return (keyword "Abort All") -- cgit v1.2.3 From bdcf5b040b975a179fe9b2889fea0d38ae4689df Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 18 Nov 2016 08:38:30 +0100 Subject: Revert "Merge remote-tracking branch 'github/pr/360' into v8.6" This reverts commit b00e039b957b8428c21faec5c76f3a3484cde2cf, reversing changes made to ca9e00ff9b2a8ee17430398a5e0bef2345c39341. It turns out that calling from fake_ide the STM commands that were removed by this PR requires an extension of the XML protocol. So postponing the integration. --- printing/ppvernac.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a6b1c97f5c..3494ad006f 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -538,6 +538,22 @@ module Make | VernacLocal (local, v) -> return (pr_locality local ++ spc() ++ pr_vernac_body v) + (* Stm *) + | VernacStm JoinDocument -> + return (keyword "Stm JoinDocument") + | VernacStm PrintDag -> + return (keyword "Stm PrintDag") + | VernacStm Finish -> + return (keyword "Stm Finish") + | VernacStm Wait -> + return (keyword "Stm Wait") + | VernacStm (Observe id) -> + return (keyword "Stm Observe " ++ str(Stateid.to_string id)) + | VernacStm (Command v) -> + return (keyword "Stm Command " ++ pr_vernac_body v) + | VernacStm (PGLast v) -> + return (keyword "Stm PGLast " ++ pr_vernac_body v) + (* Proof management *) | VernacAbortAll -> return (keyword "Abort All") -- cgit v1.2.3