# HG changeset patch
# User wenzelm
# Date 1331240680 -3600
# Node ID 8d5d255bf89c7749008d5f5aac983bc20f6962f7
# Parent  52e9770e0107d5eb18674e5f143581c0c13bef42# Parent  42e32c7775817fcd12be976a291cde7b4ef262b8
merged

diff -r 52e9770e0107 -r 8d5d255bf89c src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Thu Mar 08 16:49:24 2012 +0000
+++ b/src/Pure/PIDE/xml.ML	Thu Mar 08 22:04:40 2012 +0100
@@ -3,7 +3,7 @@
     Author:     Stefan Berghofer
     Author:     Makarius
 
-Untyped XML trees and basic data representation.
+Untyped XML trees and representation of ML values.
 *)
 
 signature XML_DATA_OPS =
@@ -28,9 +28,9 @@
 
 signature XML =
 sig
-  type attributes = Properties.T
+  type attributes = (string * string) list
   datatype tree =
-      Elem of Markup.T * tree list
+      Elem of (string * attributes) * tree list
     | Text of string
   type body = tree list
   val add_content: tree -> Buffer.T -> Buffer.T
@@ -59,10 +59,10 @@
 
 (** XML trees **)
 
-type attributes = Properties.T;
+type attributes = (string * string) list;
 
 datatype tree =
-    Elem of Markup.T * tree list
+    Elem of (string * attributes) * tree list
   | Text of string;
 
 type body = tree list;
@@ -360,8 +360,7 @@
   | node t = raise XML_BODY [t];
 
 fun vector atts =
-  #1 (fold_map (fn (a, x) =>
-        fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts 0);
+  map_index (fn (i, (a, x)) => if int_atom a = i then x else raise XML_ATOM a) atts;
 
 fun tagged (Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
   | tagged t = raise XML_BODY [t];
diff -r 52e9770e0107 -r 8d5d255bf89c src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Mar 08 16:49:24 2012 +0000
+++ b/src/Pure/PIDE/xml.scala	Thu Mar 08 22:04:40 2012 +0100
@@ -215,7 +215,7 @@
     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
     private def vector(xs: List[String]): XML.Attributes =
-      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+      xs.zipWithIndex.map({ case (x, i) => (int_atom(i), x) })
 
     private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
       XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
@@ -293,15 +293,8 @@
       }
 
     private def vector(atts: XML.Attributes): List[String] =
-    {
-      val xs = new mutable.ListBuffer[String]
-      var i = 0
-      for ((a, x) <- atts) {
-        if (int_atom(a) == i) { xs += x; i = i + 1 }
-        else throw new XML_Atom(a)
-      }
-      xs.toList
-    }
+      atts.iterator.zipWithIndex.map(
+        { case ((a, x), i) => if (int_atom(a) == i) x else throw new XML_Atom(a) }).toList
 
     private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
       t match {
diff -r 52e9770e0107 -r 8d5d255bf89c src/Pure/library.ML
--- a/src/Pure/library.ML	Thu Mar 08 16:49:24 2012 +0000
+++ b/src/Pure/library.ML	Thu Mar 08 22:04:40 2012 +0100
@@ -470,9 +470,9 @@
   let
     fun get (_: int) [] = NONE
       | get i (x :: xs) =
-          case f x
-           of NONE => get (i + 1) xs
-            | SOME y => SOME (i, y)
+          (case f x of
+            NONE => get (i + 1) xs
+          | SOME y => SOME (i, y))
   in get 0 end;
 
 val flat = List.concat;
diff -r 52e9770e0107 -r 8d5d255bf89c src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Thu Mar 08 16:49:24 2012 +0000
+++ b/src/Tools/induct_tacs.ML	Thu Mar 08 22:04:40 2012 +0100
@@ -18,12 +18,12 @@
 
 (* case analysis *)
 
-fun check_type ctxt t =
+fun check_type ctxt (t, pos) =
   let
     val u = singleton (Variable.polymorphic ctxt) t;
     val U = Term.fastype_of u;
     val _ = Term.is_TVar U andalso
-      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u);
+      error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.str_of pos);
   in (u, U) end;
 
 fun gen_case_tac ctxt0 s opt_rule i st =
@@ -34,7 +34,8 @@
         SOME rule => rule
       | NONE =>
           (case Induct.find_casesT ctxt
-              (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s))) of
+              (#2 (check_type ctxt (Proof_Context.read_term_schematic ctxt s,
+                #2 (Syntax.read_token s)))) of
             rule :: _ => rule
           | [] => @{thm case_split}));
     val _ = Method.trace ctxt [rule];
@@ -71,17 +72,22 @@
     fun induct_var name =
       let
         val t = Syntax.read_term ctxt name;
+        val (_, pos) = Syntax.read_token name;
         val (x, _) = Term.dest_Free t handle TERM _ =>
-          error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t);
+          error ("Induction argument not a variable: " ^
+            Syntax.string_of_term ctxt t ^ Position.str_of pos);
         val eq_x = fn Free (y, _) => x = y | _ => false;
         val _ =
           if Term.exists_subterm eq_x concl then ()
-          else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t);
+          else
+            error ("No such variable in subgoal: " ^
+              Syntax.string_of_term ctxt t ^ Position.str_of pos);
         val _ =
           if (exists o Term.exists_subterm) eq_x prems then
-            warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t)
+            warning ("Induction variable occurs also among premises: " ^
+              Syntax.string_of_term ctxt t ^ Position.str_of pos)
           else ();
-      in #1 (check_type ctxt t) end;
+      in #1 (check_type ctxt (t, pos)) end;
 
     val argss = map (map (Option.map induct_var)) varss;
     val rule =