--- 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];
--- 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 {
--- 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;
--- 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 =