cases: more position information and PIDE markup;

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Sep 03 13:09:15 2013 +0200
@@ -460,7 +460,7 @@
       exists (exists (curry (op =) name o shortest_name o fst)
               o datatype_constrs hol_ctxt) deep_dataTs
     val likely_in_struct_induct_step =
-      exists is_struct_induct_step (Proof_Context.cases_of ctxt)
+      exists is_struct_induct_step (Proof_Context.dest_cases ctxt)
     val _ = if standard andalso likely_in_struct_induct_step then
               pprint_nt (fn () => Pretty.blk (0,
                   pstrs "Hint: To check that the induction hypothesis is \

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 03 13:09:15 2013 +0200
@@ -1600,7 +1600,7 @@
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     val lthy'' = lthy'
       |> fold Variable.auto_fixes cases_rules
-      |> Proof_Context.add_cases true case_env
+      |> Proof_Context.update_cases true case_env
     fun after_qed thms goal_ctxt =
       let
         val global_thms = Proof_Context.export goal_ctxt

--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 03 13:09:15 2013 +0200
@@ -611,8 +611,9 @@
 val _ =
   Outer_Syntax.command @{command_spec "case"} "invoke local context"
     ((@{keyword "("} |--
-      Parse.!!! (Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
-      Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
+      Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+        --| @{keyword ")"}) ||
+      Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
         Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
 
 

--- a/src/Pure/Isar/proof.ML	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 03 13:09:15 2013 +0200
@@ -70,8 +70,10 @@
   val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val unfolding: ((thm list * attribute list) list) list -> state -> state
   val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
-  val invoke_case: string * binding option list * attribute list -> state -> state
-  val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state
+  val invoke_case: (string * Position.T) * binding option list * attribute list ->
+    state -> state
+  val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list ->
+    state -> state
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
@@ -399,8 +401,8 @@
     Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
-          (Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #>
-           Proof_Context.add_cases true meth_cases)
+          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
+           Proof_Context.update_cases true meth_cases)
           (K (statement, [], using, goal', before_qed, after_qed)) I)
   end;
 
@@ -744,17 +746,17 @@
 fun qualified_binding a =
   Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
 
-fun gen_invoke_case prep_att (name, xs, raw_atts) state =
+fun gen_invoke_case prep_att ((name, pos), xs, raw_atts) state =
   let
     val atts = map (prep_att (context_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
-      ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
+      ctxt |> Proof_Context.apply_case (Proof_Context.check_case ctxt (name, pos) xs));
     val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
   in
     state'
     |> assume assumptions
     |> bind_terms Auto_Bind.no_facts
-    |> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
+    |> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
   end;
 
 in

--- a/src/Pure/Isar/proof_context.ML	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 03 13:09:15 2013 +0200
@@ -31,7 +31,6 @@
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
   val facts_of: Proof.context -> Facts.T
-  val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
@@ -132,9 +131,10 @@
   val add_assms_i: Assumption.export ->
     (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val add_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
+  val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
+  val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
-  val get_case: Proof.context -> string -> binding option list -> Rule_Cases.T
+  val check_case: Proof.context -> string * Position.T -> binding option list -> Rule_Cases.T
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -192,6 +192,9 @@
 
 (** Isar proof context information **)
 
+type cases = ((Rule_Cases.T * bool) * int) Name_Space.table;
+val empty_cases: cases = Name_Space.empty_table Markup.caseN;
+
 datatype data =
   Data of
    {mode: mode,                  (*inner syntax mode*)
@@ -199,7 +202,7 @@
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts*)
-    cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
+    cases: cases};               (*named case contexts: case, is_proper, running index*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
   Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
@@ -210,7 +213,7 @@
   fun init thy =
     make_data (mode_default, Local_Syntax.init thy,
       (Sign.tsig_of thy, Sign.tsig_of thy),
-      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
+      (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, empty_cases);
 );
 
 fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
@@ -1132,28 +1135,23 @@
 
 (** cases **)
 
+fun dest_cases ctxt =
+  Symtab.fold (fn (a, (c, i)) => cons (i, (a, c))) (#2 (cases_of ctxt)) []
+  |> sort (int_ord o pairself #1) |> map #2;
+
 local
 
-fun rem_case name = remove (fn (x: string, (y, _)) => x = y) name;
-
-fun add_case _ ("", _) cases = cases
-  | add_case _ (name, NONE) cases = rem_case name cases
-  | add_case is_proper (name, SOME c) cases = (name, (c, is_proper)) :: rem_case name cases;
-
-fun prep_case name fxs c =
-  let
-    fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
-      | replace [] ys = ys
-      | replace (_ :: _) [] = error ("Too many parameters for case " ^ quote name);
-    val Rule_Cases.Case {fixes, assumes, binds, cases} = c;
-    val fixes' = replace fxs fixes;
-    val binds' = map drop_schematic binds;
-  in
-    if null (fold (Term.add_tvarsT o snd) fixes []) andalso
-      null (fold (fold Term.add_vars o snd) assumes []) then
-        Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
-    else error ("Illegal schematic variable(s) in case " ^ quote name)
-  end;
+fun update_case _ _ ("", _) res = res
+  | update_case _ _ (name, NONE) ((space, tab), index) =
+      let
+        val tab' = Symtab.delete_safe name tab;
+      in ((space, tab'), index) end
+  | 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 index' = index + 1;
+      in (cases', index') end;
 
 fun fix (b, T) ctxt =
   let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
@@ -1161,7 +1159,13 @@
 
 in
 
-fun add_cases is_proper = map_cases o fold (add_case is_proper);
+fun update_cases is_proper args ctxt =
+  let
+    val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming);
+    val cases = cases_of ctxt;
+    val index = Symtab.fold (fn _ => Integer.add 1) (#2 cases) 0;
+    val (cases', _) = fold (update_case context is_proper) args (cases, index);
+  in map_cases (K cases') ctxt end;
 
 fun case_result c ctxt =
   let
@@ -1171,16 +1175,29 @@
   in
     ctxt'
     |> bind_terms (map drop_schematic binds)
-    |> add_cases true (map (apsnd SOME) cases)
+    |> update_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;
 
 val apply_case = apfst fst oo case_result;
 
-fun get_case ctxt name xs =
-  (case AList.lookup (op =) (cases_of ctxt) name of
-    NONE => error ("Unknown case: " ^ quote name)
-  | SOME (c, _) => prep_case name xs c);
+fun check_case ctxt (name, pos) fxs =
+  let
+    val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, _), _)) =
+      Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
+
+    fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
+      | replace [] ys = ys
+      | replace (_ :: _) [] =
+          error ("Too many parameters for case " ^ quote name ^ Position.here pos);
+    val fixes' = replace fxs fixes;
+    val binds' = map drop_schematic binds;
+  in
+    if null (fold (Term.add_tvarsT o snd) fixes []) andalso
+      null (fold (fold Term.add_vars o snd) assumes []) then
+        Rule_Cases.Case {fixes = fixes', assumes = assumes, binds = binds', cases = cases}
+    else error ("Illegal schematic variable(s) in case " ^ quote name ^ Position.here pos)
+  end;
 
 end;
 
@@ -1278,10 +1295,10 @@
 
 fun pretty_cases ctxt =
   let
-    fun add_case (_, (_, false)) = I
-      | add_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
-          cons (name, (fixes, case_result c ctxt));
-    val cases = fold add_case (cases_of ctxt) [];
+    fun mk_case (_, (_, false)) = NONE
+      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
+          SOME (name, (fixes, case_result c ctxt));
+    val cases = dest_cases ctxt |> map_filter mk_case;
   in
     if null cases then []
     else [Pretty.big_list "cases:" (map pretty_case cases)]

--- a/src/Pure/PIDE/markup.ML	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 03 13:09:15 2013 +0200
@@ -46,6 +46,7 @@
   val type_nameN: string
   val constantN: string
   val fixedN: string val fixed: string -> T
+  val caseN: string val case_: string -> T
   val dynamic_factN: string val dynamic_fact: string -> T
   val tfreeN: string val tfree: T
   val tvarN: string val tvar: T
@@ -288,6 +289,7 @@
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" nameN;
+val (caseN, case_) = markup_string "case" nameN;
 val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN;
 
 

--- a/src/Pure/PIDE/markup.scala	Tue Sep 03 11:58:34 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Sep 03 13:09:15 2013 +0200
@@ -105,8 +105,8 @@
   val CLASS = "class"
   val TYPE_NAME = "type_name"
   val FIXED = "fixed"
+  val CASE = "case"
   val CONSTANT = "constant"
-
   val DYNAMIC_FACT = "dynamic_fact"