conceal improper cases, e.g. relevant for completion (and potentially for markup);
--- a/src/Pure/Isar/proof_context.ML Fri Mar 14 15:12:22 2014 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Mar 14 15:26:52 2014 +0100
@@ -1167,8 +1167,11 @@
(Name_Space.del_table name cases, index)
| update_case context is_proper (name, SOME c) (cases, index) =
let
- val (_, cases') = cases |> Name_Space.define context false
- (Binding.make (name, Position.none), ((c, is_proper), index));
+ val binding =
+ Binding.make (name, Position.none)
+ |> not is_proper ? Binding.conceal;
+ val (_, cases') = cases
+ |> Name_Space.define context false (binding, ((c, is_proper), index));
val index' = index + 1;
in (cases', index') end;