improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
tuned;

--- a/NEWS	Thu Jan 05 15:31:49 2012 +0100
+++ b/NEWS	Thu Jan 05 18:18:39 2012 +0100
@@ -60,6 +60,12 @@
 
 *** HOL ***
 
+* Concrete syntax for case expressions includes constraints for source
+positions, and thus produces Prover IDE markup for its bindings.
+INCOMPATIBILITY for old-style syntax translations that augment the
+pattern notation; e.g. see src/HOL/HOLCF/One.thy for translations of
+one_case.
+
 * Finite_Set.fold now qualified.  INCOMPATIBILITY.
 
 * Renamed some facts on canonical fold on lists, in order to avoid problems

--- a/src/HOL/HOL.thy	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/HOL.thy	Thu Jan 05 18:18:39 2012 +0100
@@ -104,34 +104,31 @@
 notation (xsymbols)
   iff  (infixr "\<longleftrightarrow>" 25)
 
-nonterminal letbinds and letbind
-nonterminal case_pat and case_syn and cases_syn
+syntax
+  "_The" :: "[pttrn, bool] => 'a"  ("(3THE _./ _)" [0, 10] 10)
+translations
+  "THE x. P" == "CONST The (%x. P)"
+print_translation {*
+  [(@{const_syntax The}, fn [Abs abs] =>
+      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
+      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
+*}  -- {* To avoid eta-contraction of body *}
 
+nonterminal letbinds and letbind
 syntax
-  "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)
-
   "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
   ""            :: "letbind => letbinds"                 ("_")
   "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
   "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" [0, 10] 10)
 
-  "_case_syntax"      :: "['a, cases_syn] => 'b"              ("(case _ of/ _)" 10)
-  "_case1"            :: "[case_pat, 'b] => case_syn"         ("(2_ =>/ _)" 10)
-  ""                  :: "case_syn => cases_syn"              ("_")
-  "_case2"            :: "[case_syn, cases_syn] => cases_syn" ("_/ | _")
-  "_strip_positions"  :: "'a => case_pat"                     ("_")
-
+nonterminal case_syn and cases_syn
+syntax
+  "_case_syntax" :: "['a, cases_syn] => 'b"  ("(case _ of/ _)" 10)
+  "_case1" :: "['a, 'b] => case_syn"  ("(2_ =>/ _)" 10)
+  "" :: "case_syn => cases_syn"  ("_")
+  "_case2" :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")
 syntax (xsymbols)
-  "_case1" :: "[case_pat, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
-
-translations
-  "THE x. P"              == "CONST The (%x. P)"
-
-print_translation {*
-  [(@{const_syntax The}, fn [Abs abs] =>
-      let val (x, t) = Syntax_Trans.atomic_abs_tr' abs
-      in Syntax.const @{syntax_const "_The"} $ x $ t end)]
-*}  -- {* To avoid eta-contraction of body *}
+  "_case1" :: "['a, 'b] => case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
 
 notation (xsymbols)
   All  (binder "\<forall>" 10) and

--- a/src/HOL/HOLCF/One.thy	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/HOLCF/One.thy	Thu Jan 05 18:18:39 2012 +0100
@@ -58,6 +58,7 @@
 
 translations
   "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x"
+  "case x of XCONST ONE :: 'a \<Rightarrow> t" => "CONST one_case\<cdot>t\<cdot>x"
   "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t"
 
 lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>"

--- a/src/HOL/HOLCF/Ssum.thy	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/HOLCF/Ssum.thy	Thu Jan 05 18:18:39 2012 +0100
@@ -168,6 +168,7 @@
 
 translations
   "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+  "case s of (XCONST sinl :: 'a)\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" => "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
 
 translations
   "\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"

--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Thu Jan 05 18:18:39 2012 +0100
@@ -452,27 +452,35 @@
       val cabs = app "_cabs"
       val capp = app @{const_syntax Rep_cfun}
       val capps = Library.foldl capp
-      fun con1 authentic n (con,args) =
+      fun con1 authentic n (con, args) =
           Library.foldl capp (c_ast authentic con, argvars n args)
-      fun case1 authentic (n, c) =
-          app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
+      fun con1_constraint authentic n (con, args) =
+          Library.foldl capp
+            (Ast.Appl
+              [Ast.Constant @{syntax_const "_constrain"}, c_ast authentic con,
+                Ast.Variable ("'a" ^ string_of_int n)],
+             argvars n args)
+      fun case1 constraint authentic (n, c) =
+        app @{syntax_const "_case1"}
+          ((if constraint then con1_constraint else con1) authentic n c, expvar n)
       fun arg1 (n, (_, args)) = List.foldr cabs (expvar n) (argvars n args)
       fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
       val case_constant = Ast.Constant (syntax (case_const dummyT))
-      fun case_trans authentic =
-        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+      fun case_trans constraint authentic =
           (app "_case_syntax"
             (Ast.Variable "x",
-             foldr1 (app "_case2") (map_index (case1 authentic) spec)),
+             foldr1 (app @{syntax_const "_case2"}) (map_index (case1 constraint authentic) spec)),
            capp (capps (case_constant, map_index arg1 spec), Ast.Variable "x"))
       fun one_abscon_trans authentic (n, c) =
-        (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
-          (cabs (con1 authentic n c, expvar n),
-           capps (case_constant, map_index (when1 n) spec))
+          (if authentic then Syntax.Parse_Print_Rule else Syntax.Parse_Rule)
+            (cabs (con1 authentic n c, expvar n),
+             capps (case_constant, map_index (when1 n) spec))
       fun abscon_trans authentic =
           map_index (one_abscon_trans authentic) spec
       val trans_rules : Ast.ast Syntax.trrule list =
-          case_trans false :: case_trans true ::
+          Syntax.Parse_Print_Rule (case_trans false true) ::
+          Syntax.Parse_Rule (case_trans false false) ::
+          Syntax.Parse_Rule (case_trans true false) ::
           abscon_trans false @ abscon_trans true
     in
       val thy = Sign.add_trrules trans_rules thy

--- a/src/HOL/HOLCF/Up.thy	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/HOLCF/Up.thy	Thu Jan 05 18:18:39 2012 +0100
@@ -181,6 +181,7 @@
 
 translations
   "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+  "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
   "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
 
 text {* continuous versions of lemmas for @{typ "('a)u"} *}

--- a/src/HOL/List.thy	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/List.thy	Thu Jan 05 18:18:39 2012 +0100
@@ -386,7 +386,7 @@
       (* FIXME proper name context!? *)
       val x = Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
       val e = if opti then singl e else e;
-      val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
+      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
       val case2 =
         Syntax.const @{syntax_const "_case1"} $
           Syntax.const @{const_syntax dummy_pattern} $ NilC;

--- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jan 05 15:31:49 2012 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Jan 05 18:18:39 2012 +0100
@@ -3,6 +3,9 @@
     Author:     Stefan Berghofer, TU Muenchen
 
 Datatype package: nested case expressions on datatypes.
+
+TODO: generic tool with separate data slot, without hard-wiring the
+datatype package.
 *)
 
 signature DATATYPE_CASE =
@@ -57,25 +60,30 @@
       strip_constraints t ||> cons tT
   | strip_constraints t = (t, []);
 
-fun mk_fun_constrain tT t =
-  Syntax.const @{syntax_const "_constrain"} $ t $
-    (Syntax.const @{type_syntax fun} $ tT $ Syntax.const @{type_syntax dummy});
+fun constrain_Abs tT t = Syntax.const @{syntax_const "_constrainAbs"} $ t $ tT;
 
 
 (*Produce an instance of a constructor, plus fresh variables for its arguments.*)
 fun fresh_constr ty_match ty_inst colty used c =
   let
-    val (_, Ty) = dest_Const c;
-    val Ts = binder_types Ty;
+    val (_, T) = dest_Const c;
+    val Ts = binder_types T;
     val names =
       Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts));
-    val ty = body_type Ty;
+    val ty = body_type T;
     val ty_theta = ty_match ty colty
       handle Type.TYPE_MATCH => raise CASE_ERROR ("type mismatch", ~1);
     val c' = ty_inst ty_theta c;
     val gvars = map (ty_inst ty_theta o Free) (names ~~ Ts);
   in (c', gvars) end;
 
+fun strip_comb_positions tm =
+  let
+    fun result t ts = (Term_Position.strip_positions t, ts);
+    fun strip (t as (Const (@{syntax_const "_constrain"}, _) $ _ $ _)) ts = result t ts
+      | strip (f $ t) ts = strip f (t :: ts)
+      | strip t ts = result t ts;
+  in strip tm [] end;
 
 (*Go through a list of rows and pick out the ones beginning with a
   pattern with constructor = name.*)
@@ -83,7 +91,7 @@
   let val k = length (binder_types T) in
     fold (fn (row as ((prfx, p :: ps), rhs as (_, i))) =>
       fn ((in_group, not_in_group), (names, cnstrts)) =>
-        (case strip_comb p of
+        (case strip_comb_positions p of
           (Const (name', _), args) =>
             if name = name' then
               if length args = k then
@@ -162,7 +170,8 @@
       | mk path (rows as ((row as ((_, [Free _]), _)) :: _ :: _)) = mk path [row]
       | mk (u :: us) (rows as ((_, _ :: _), _) :: _) =
           let val col0 = map (fn ((_, p :: _), (_, i)) => (p, i)) rows in
-            (case Option.map (apfst head_of) (find_first (not o is_Free o fst) col0) of
+            (case Option.map (apfst (fst o strip_comb_positions))
+                (find_first (not o is_Free o fst) col0) of
               NONE =>
                 let
                   val rows' = map (fn ((v, _), row) => row ||>
@@ -186,7 +195,7 @@
                         map2 (fn {new_formals, names, constraints, ...} =>
                           fold_rev (fn ((x as Free (_, T), s), cnstrts) => fn t =>
                             Abs (if s = "" then name else s, T, abstract_over (x, t))
-                            |> fold mk_fun_constrain cnstrts) (new_formals ~~ names ~~ constraints))
+                            |> fold constrain_Abs cnstrts) (new_formals ~~ names ~~ constraints))
                         subproblems dtrees;
                       val types = map type_of (case_functions @ [u]);
                       val case_const = Const (case_name, types ---> range_ty);
@@ -210,7 +219,7 @@
           case_error (quote s ^ " occurs repeatedly in the pattern " ^
             quote (Syntax.string_of_term ctxt pat))
         else x :: xs)
-    | _ => I) pat [];
+    | _ => I) (Term_Position.strip_positions pat) [];
 
 fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
   let
@@ -432,7 +441,8 @@
                 | Const (s, _) => Syntax.const (Lexicon.mark_const s)
                 | t => t) pat $
             map_aterms
-              (fn x as Free (s, T) => if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
+              (fn x as Free (s, T) =>
+                  if member (op =) xs (s, T) then Syntax_Trans.mark_bound s else x
                 | t => t) rhs
         end;
     in