# HG changeset patch
# User wenzelm
# Date 1282232512 -7200
# Node ID befdd6833ec0e890a81d57dbaa9602a2ab12842d
# Parent  32ad17fe2b9c0bb86faf11fd644b5d33b6fb5f4e# Parent  f5bbfc019937705984a29f307959935e2e5e9272
merged

diff -r 32ad17fe2b9c -r befdd6833ec0 Admin/polyml/README
--- a/Admin/polyml/README	Thu Aug 19 16:08:59 2010 +0200
+++ b/Admin/polyml/README	Thu Aug 19 17:41:52 2010 +0200
@@ -1,27 +1,15 @@
-
-This distribution of Poly/ML 5.3 is based on the original
-polyml.5.3.tar.gz from http://www.polyml.org with some minimal changes:
+Poly/ML for Isabelle
+====================
 
-diff polyml.5.3/libpolyml/processes.cpp-orig polyml.5.3/libpolyml/processes.cpp
-995,996c995,996
-<     // we set this to 100ms so that we're not waiting too long.
-<     if (maxMillisecs > 100) maxMillisecs = 100;
----
->     // we set this to 10ms so that we're not waiting too long.
->     if (maxMillisecs > 10) maxMillisecs = 10;
+This distribution of Poly/ML 5.4 has been compiled from the original
+sources using the included build script.  For example:
 
-
-Then it is compiled as follows:
+  ./build polyml.5.4 x86-linux --with-gmp
 
-  cd polyml.5.3
-  ./configure --prefix="$HOME/tmp/polyml"
-  make
-  make install
-
-
-Now $HOME/tmp/polyml/bin/* and $HOME/tmp/polyml/lib/* are moved to the
-platform-specific target directory (e.g. polyml-5.3.0/x86-linux).
+The resulting executables and shared libraries are moved to
+x86-linux/.  This directory layout accomodates the standard ML_HOME
+settings for Isabelle.
 
 
 	Makarius
-	26-May-2010
+	17-Aug-2010
diff -r 32ad17fe2b9c -r befdd6833ec0 Admin/polyml/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/build	Thu Aug 19 17:41:52 2010 +0200
@@ -0,0 +1,85 @@
+#!/usr/bin/env bash
+#
+# Multi-platform build script for Poly/ML
+
+THIS="$(cd "$(dirname "$0")"; pwd)"
+PRG="$(basename "$0")"
+
+
+# diagnostics
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
+  echo
+  echo "  Build Poly/ML in SOURCE directory for given platform in TARGET,"
+  echo "  using the usual Isabelle platform identifiers."
+  echo
+  echo "  Additional options for ./configure may be given, e.g. --with-gmp"
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+# command line args
+
+[ "$#" -eq 0 ] && usage
+SOURCE="$1"; shift
+
+[ "$#" -eq 0 ] && usage
+TARGET="$1"; shift
+
+USER_OPTIONS=("$@")
+
+
+# main
+
+[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
+
+case "$TARGET" in
+  x86-linux)
+    OPTIONS=()
+    ;;
+  x86_64-linux)
+    OPTIONS=()
+    ;;
+  x86-darwin)
+    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
+      CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3')
+    ;;
+  x86_64-darwin)
+    OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
+      CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64')
+    ;;
+  x86-cygwin)
+    OPTIONS=()
+    ;;
+  ppc-darwin | sparc-solaris | x86-solaris | x86-bsd)
+    OPTIONS=()
+    ;;
+  *)
+    fail "Bad platform identifier: \"$TARGET\""
+    ;;
+esac
+
+(
+  cd "$SOURCE"
+  make distclean
+
+  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
+    make compiler && \
+    make install; } || fail "Build failed"
+)
+
+mkdir -p "$TARGET"
+mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
+mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
+rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
+rm -rf "$SOURCE/$TARGET/share"
diff -r 32ad17fe2b9c -r befdd6833ec0 NEWS
--- a/NEWS	Thu Aug 19 16:08:59 2010 +0200
+++ b/NEWS	Thu Aug 19 17:41:52 2010 +0200
@@ -172,6 +172,11 @@
 change in semantics.
 
 
+*** System ***
+
+* Discontinued support for Poly/ML 5.0 and 5.1 versions.
+
+
 
 New in Isabelle2009-2 (June 2010)
 ---------------------------------
diff -r 32ad17fe2b9c -r befdd6833ec0 README
--- a/README	Thu Aug 19 16:08:59 2010 +0200
+++ b/README	Thu Aug 19 17:41:52 2010 +0200
@@ -13,7 +13,7 @@
    Windows with Cygwin, Mac OS) and depends on the following main
    add-on tools:
 
-     * The Poly/ML compiler and runtime system (version 5.x).
+     * The Poly/ML compiler and runtime system (version 5.2.1 or later).
      * The GNU bash shell (version 3.x or 2.x).
      * Perl (version 5.x).
      * GNU Emacs (version 22) -- for the Proof General interface.
diff -r 32ad17fe2b9c -r befdd6833ec0 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Aug 19 16:08:59 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Aug 19 17:41:52 2010 +0200
@@ -97,7 +97,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "string option -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
@@ -114,13 +114,13 @@
   with operations on expecting a regular @{text "ctxt:"}~@{ML_type
   Proof.context}.
 
-  \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a
-  trivial local theory from the given background theory.
-  Alternatively, @{text "SOME name"} may be given to initialize a
-  @{command locale} or @{command class} context (a fully-qualified
-  internal name is expected here).  This is useful for experimentation
-  --- normally the Isar toplevel already takes care to initialize the
-  local theory context.
+  \item @{ML Named_Target.init}~@{text "name thy"} initializes a local
+  theory derived from the given background theory.  An empty name
+  refers to a \emph{global theory} context, and a non-empty name
+  refers to a @{command locale} or @{command class} context (a
+  fully-qualified internal name is expected here).  This is useful for
+  experimentation --- normally the Isar toplevel already takes care to
+  initialize the local theory context.
 
   \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
   lthy"} defines a local entity according to the specification that is
diff -r 32ad17fe2b9c -r befdd6833ec0 doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Aug 19 16:08:59 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Aug 19 17:41:52 2010 +0200
@@ -123,7 +123,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
-  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex]
+  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex]
   \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
 \verb|    local_theory -> (term * (string * thm)) * local_theory| \\
   \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
@@ -139,13 +139,13 @@
   any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
   with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
 
-  \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a
-  trivial local theory from the given background theory.
-  Alternatively, \isa{SOME\ name} may be given to initialize a
-  \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
-  internal name is expected here).  This is useful for experimentation
-  --- normally the Isar toplevel already takes care to initialize the
-  local theory context.
+  \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local
+  theory derived from the given background theory.  An empty name
+  refers to a \emph{global theory} context, and a non-empty name
+  refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a
+  fully-qualified internal name is expected here).  This is useful for
+  experimentation --- normally the Isar toplevel already takes care to
+  initialize the local theory context.
 
   \item \verb|Local_Theory.define|~\isa{{\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
   given relatively to the current \isa{lthy} context.  In
diff -r 32ad17fe2b9c -r befdd6833ec0 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Aug 19 16:08:59 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Thu Aug 19 17:41:52 2010 +0200
@@ -8,8 +8,6 @@
   '("\\."
     "\\.\\."
     "Isabelle\\.command"
-    "Isar\\.define_command"
-    "Isar\\.edit_document"
     "ML"
     "ML_command"
     "ML_prf"
@@ -256,8 +254,6 @@
 
 (defconst isar-keywords-control
   '("Isabelle\\.command"
-    "Isar\\.define_command"
-    "Isar\\.edit_document"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
diff -r 32ad17fe2b9c -r befdd6833ec0 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Aug 19 16:08:59 2010 +0200
+++ b/etc/isar-keywords.el	Thu Aug 19 17:41:52 2010 +0200
@@ -8,8 +8,6 @@
   '("\\."
     "\\.\\."
     "Isabelle\\.command"
-    "Isar\\.define_command"
-    "Isar\\.edit_document"
     "ML"
     "ML_command"
     "ML_prf"
@@ -320,8 +318,6 @@
 
 (defconst isar-keywords-control
   '("Isabelle\\.command"
-    "Isar\\.define_command"
-    "Isar\\.edit_document"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
diff -r 32ad17fe2b9c -r befdd6833ec0 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# Poly/ML 5.0 startup script.
-
-export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
-
-
-## diagnostics
-
-function fail_out()
-{
-  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
-  exit 2
-}
-
-function check_file()
-{
-  if [ ! -f "$1" ]; then
-    echo "Unable to locate $1" >&2
-    echo "Please check your ML system settings!" >&2
-    exit 2
-  fi
-}
-
-
-## compiler executables and libraries
-
-POLY="$ML_HOME/poly"
-check_file "$POLY"
-
-if [ "$(basename "$ML_HOME")" = bin ]; then
-  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
-else
-  POLYLIB="$ML_HOME"
-fi
-
-export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
-export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
-
-
-## prepare databases
-
-if [ -z "$INFILE" ]; then
-  PRG="$POLY"
-  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
-else
-  check_file "$INFILE"
-  PRG="$INFILE"
-  EXIT=""
-fi
-
-if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
-else
-  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
-  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  rm -f "${OUTFILE}.o" || fail_out
-fi
-
-
-## run it!
-
-MLTEXT="$EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
-
-if [ -z "$TERMINATE" ]; then
-  FEEDER_OPTS=""
-else
-  FEEDER_OPTS="-q"
-fi
-
-"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
-  { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
-RC="$?"
-
-if [ -n "$OUTFILE" ]; then
-  if [ -e "${OUTFILE}.o" ]; then
-    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out
-    rm -f "${OUTFILE}.o"
-    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
-  fi
-  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
-fi
-
-exit "$RC"
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/markup.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -9,8 +9,8 @@
   val parse_int: string -> int
   val print_int: int -> string
   type T = string * Properties.T
-  val none: T
-  val is_none: T -> bool
+  val empty: T
+  val is_empty: T -> bool
   val properties: Properties.T -> T -> T
   val nameN: string
   val name: string -> T -> T
@@ -142,10 +142,10 @@
 
 type T = string * Properties.T;
 
-val none = ("", []);
+val empty = ("", []);
 
-fun is_none ("", _) = true
-  | is_none _ = false;
+fun is_empty ("", _) = true
+  | is_empty _ = false;
 
 
 fun properties more_props ((elem, props): T) =
@@ -356,7 +356,7 @@
     the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
 end;
 
-fun output m = if is_none m then no_output else #output (get_mode ()) m;
+fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
 val enclose = output #-> Library.enclose;
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/markup.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -48,6 +48,11 @@
   }
 
 
+  /* empty */
+
+  val Empty = Markup("", Nil)
+
+
   /* name */
 
   val NAME = "name"
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/position.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -20,13 +20,13 @@
   def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
   def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
 
-  def get_range(pos: T): Option[(Int, Int)] =
+  def get_range(pos: T): Option[Text.Range] =
     (get_offset(pos), get_end_offset(pos)) match {
-      case (Some(begin), Some(end)) => Some(begin, end)
-      case (Some(begin), None) => Some(begin, begin + 1)
+      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
+      case (Some(start), None) => Some(Text.Range(start, start + 1))
       case (None, _) => None
     }
 
   object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
-  object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
+  object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
 }
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/pretty.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -132,7 +132,7 @@
 
 fun markup_block m arg = block_markup (Markup.output m) arg;
 
-val blk = markup_block Markup.none;
+val blk = markup_block Markup.empty;
 fun block prts = blk (2, prts);
 val strs = block o breaks o map str;
 
@@ -142,7 +142,7 @@
 fun command name = mark Markup.command (str name);
 
 fun markup_chunks m prts = markup m (fbreaks prts);
-val chunks = markup_chunks Markup.none;
+val chunks = markup_chunks Markup.empty;
 fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
 
 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/sha1.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sha1.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -0,0 +1,28 @@
+/*  Title:      Pure/General/sha1.scala
+    Author:     Makarius
+
+Digesting strings according to SHA-1 (see RFC 3174).
+*/
+
+package isabelle
+
+
+import java.security.MessageDigest
+
+
+object SHA1
+{
+  def digest_bytes(bytes: Array[Byte]): String =
+  {
+    val result = new StringBuilder
+    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
+      val i = b.asInstanceOf[Int] & 0xFF
+      if (i < 16) result += '0'
+      result ++= Integer.toHexString(i)
+    }
+    result.toString
+  }
+
+  def digest(s: String): String = digest_bytes(Standard_System.string_bytes(s))
+}
+
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/symbol.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -106,8 +106,9 @@
       }
       buf.toArray
     }
-    def decode(sym: Int): Int =
+    def decode(sym1: Int): Int =
     {
+      val sym = sym1 - 1
       val end = index.length
       def bisect(a: Int, b: Int): Int =
       {
@@ -123,6 +124,7 @@
       if (i < 0) sym
       else index(i).chr + sym - index(i).sym
     }
+    def decode(range: Text.Range): Text.Range = range.map(decode(_))
   }
 
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/xml.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -79,7 +79,7 @@
   end;
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then Markup.no_output
+  if Markup.is_empty markup then Markup.no_output
   else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
 
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/xml.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -67,30 +67,15 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* iterate over content */
-
-  private type State = Option[(String, List[Tree])]
+  /* text content */
 
-  private def get_next(tree: Tree): State = tree match {
-    case Elem(_, body) => get_nexts(body)
-    case Text(content) => Some(content, Nil)
-  }
-  private def get_nexts(trees: List[Tree]): State = trees match {
-    case Nil => None
-    case t :: ts => get_next(t) match {
-      case None => get_nexts(ts)
-      case Some((s, r)) => Some((s, r ++ ts))
+  def content_stream(tree: Tree): Stream[String] =
+    tree match {
+      case Elem(_, body) => body.toStream.flatten(content_stream(_))
+      case Text(content) => Stream(content)
     }
-  }
 
-  def content(tree: Tree) = new Iterator[String] {
-    private var state = get_next(tree)
-    def hasNext() = state.isDefined
-    def next() = state match {
-      case Some((s, rest)) => { state = get_nexts(rest); s }
-      case None => throw new NoSuchElementException("next on empty iterator")
-    }
-  }
+  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
 
 
   /* pipe-lined cache for partial sharing */
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/yxml.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -52,7 +52,7 @@
 (* output *)
 
 fun output_markup (markup as (name, atts)) =
-  if Markup.is_none markup then Markup.no_output
+  if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
 fun element name atts body =
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/General/yxml.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -85,7 +85,7 @@
     /* stack operations */
 
     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
+    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
 
     def add(x: XML.Tree)
     {
@@ -101,7 +101,7 @@
     def pop()
     {
       (stack: @unchecked) match {
-        case ((Markup("", _), _) :: _) => err_unbalanced("")
+        case ((Markup.Empty, _) :: _) => err_unbalanced("")
         case ((markup, body) :: pending) =>
           stack = pending
           add(XML.Elem(markup, body.toList))
@@ -122,7 +122,7 @@
       }
     }
     stack match {
-      case List((Markup("", _), body)) => body.toList
+      case List((Markup.Empty, body)) => body.toList
       case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
   }
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/IsaMakefile	Thu Aug 19 17:41:52 2010 +0200
@@ -21,7 +21,6 @@
 
 BOOTSTRAP_FILES = 					\
   ML-Systems/bash.ML 					\
-  ML-Systems/compiler_polyml-5.0.ML			\
   ML-Systems/compiler_polyml-5.2.ML			\
   ML-Systems/compiler_polyml-5.3.ML			\
   ML-Systems/ml_name_space.ML				\
@@ -29,8 +28,6 @@
   ML-Systems/multithreading.ML				\
   ML-Systems/multithreading_polyml.ML			\
   ML-Systems/overloading_smlnj.ML			\
-  ML-Systems/polyml-5.0.ML				\
-  ML-Systems/polyml-5.1.ML				\
   ML-Systems/polyml-5.2.1.ML				\
   ML-Systems/polyml-5.2.ML				\
   ML-Systems/polyml.ML					\
@@ -160,6 +157,7 @@
   ML/ml_syntax.ML					\
   ML/ml_thms.ML						\
   PIDE/document.ML					\
+  PIDE/isar_document.ML					\
   Proof/extraction.ML					\
   Proof/proof_rewrite_rules.ML				\
   Proof/proof_syntax.ML					\
@@ -191,7 +189,6 @@
   Syntax/type_ext.ML					\
   System/isabelle_process.ML				\
   System/isar.ML					\
-  System/isar_document.ML				\
   System/session.ML					\
   Thy/html.ML						\
   Thy/latex.ML						\
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -16,6 +16,8 @@
   protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
   lazy val completion: Completion = new Completion + symbols  // FIXME !?
 
+  def keyword_kind(name: String): Option[String] = keywords.get(name)
+
   def + (name: String, kind: String): Outer_Syntax =
   {
     val new_keywords = keywords + (name -> kind)
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/Isar/toplevel.scala
--- a/src/Pure/Isar/toplevel.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/Isar/toplevel.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -15,16 +15,18 @@
   case object Finished extends Status
   case object Failed extends Status
 
-  def command_status(markup: List[Markup]): Status =
+  def command_status(markup: XML.Body): Status =
   {
     val forks = (0 /: markup) {
-      case (i, Markup(Markup.FORKED, _)) => i + 1
-      case (i, Markup(Markup.JOINED, _)) => i - 1
+      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
+      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
       case (i, _) => i
     }
     if (forks != 0) Forked(forks)
-    else if (markup.exists(_.name == Markup.FAILED)) Failed
-    else if (markup.exists(_.name == Markup.FINISHED)) Finished
+    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
+      Failed
+    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
+      Finished
     else Unprocessed
   }
 }
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ML-Systems/compiler_polyml-5.0.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
-
-Runtime compilation for Poly/ML 5.0 and 5.1.
-*)
-
-fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
-  let
-    val in_buffer = Unsynchronized.ref (explode (tune_source txt));
-    val out_buffer = Unsynchronized.ref ([]: string list);
-    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
-
-    val current_line = Unsynchronized.ref line;
-    fun get () =
-      (case ! in_buffer of
-        [] => ""
-      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
-    fun put s = out_buffer := s :: ! out_buffer;
-
-    fun exec () =
-      (case ! in_buffer of
-        [] => ()
-      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
-  in
-    exec () handle exn => (error (output ()); reraise exn);
-    if verbose then print (output ()) else ()
-  end;
-
-fun use_file context verbose name =
-  let
-    val instream = TextIO.openIn name;
-    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context (1, name) verbose txt end;
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ML-Systems/compiler_polyml-5.3.ML
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
 
-Runtime compilation for Poly/ML 5.3.0.
+Runtime compilation for Poly/ML 5.3 and 5.4.
 *)
 
 local
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-5.0.ML
-
-Compatibility wrapper for Poly/ML 5.0.
-*)
-
-fun reraise exn = raise exn;
-
-use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/universal.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/compiler_polyml-5.0.ML";
-use "ML-Systems/pp_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-(*  Title:      Pure/ML-Systems/polyml-5.1.ML
-
-Compatibility wrapper for Poly/ML 5.1.
-*)
-
-fun reraise exn = raise exn;
-
-use "ML-Systems/unsynchronized.ML";
-use "ML-Systems/thread_dummy.ML";
-use "ML-Systems/ml_name_space.ML";
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/compiler_polyml-5.0.ML";
-use "ML-Systems/pp_polyml.ML";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -1,6 +1,6 @@
 (*  Title:      Pure/ML-Systems/polyml.ML
 
-Compatibility wrapper for Poly/ML 5.3.0.
+Compatibility wrapper for Poly/ML 5.3 and 5.4.
 *)
 
 use "ML-Systems/unsynchronized.ML";
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -100,10 +100,10 @@
   | Real      => Markup.ML_numeral
   | Char      => Markup.ML_char
   | String    => Markup.ML_string
-  | Space     => Markup.none
+  | Space     => Markup.empty
   | Comment   => Markup.ML_comment
   | Error _   => Markup.ML_malformed
-  | EOF       => Markup.none;
+  | EOF       => Markup.empty;
 
 fun token_markup kind x =
   if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -27,9 +27,9 @@
 
   case class State(
     val command: Command,
-    val status: List[Markup],
+    val status: List[XML.Tree],
     val reverse_results: List[XML.Tree],
-    val markup: Markup_Text)
+    val markup: Markup_Tree)
   {
     /* content */
 
@@ -37,23 +37,27 @@
 
     def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
 
-    def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
+    def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
+
+    def markup_root_node: Markup_Tree.Node =
+      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
+    def markup_root: Markup_Tree = markup + markup_root_node
 
 
     /* markup */
 
-    lazy val highlight: Markup_Text =
+    lazy val highlight: List[Markup_Tree.Node] =
     {
       markup.filter(_.info match {
         case Command.HighlightInfo(_, _) => true
         case _ => false
-      })
+      }).flatten(markup_root_node)
     }
 
-    private lazy val types: List[Markup_Node] =
+    private lazy val types: List[Markup_Tree.Node] =
       markup.filter(_.info match {
         case Command.TypeInfo(_) => true
-        case _ => false }).flatten
+        case _ => false }).flatten(markup_root_node)
 
     def type_at(pos: Text.Offset): Option[String] =
     {
@@ -67,12 +71,12 @@
       }
     }
 
-    private lazy val refs: List[Markup_Node] =
+    private lazy val refs: List[Markup_Tree.Node] =
       markup.filter(_.info match {
         case Command.RefInfo(_, _, _, _) => true
-        case _ => false }).flatten
+        case _ => false }).flatten(markup_root_node)
 
-    def ref_at(pos: Text.Offset): Option[Markup_Node] =
+    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
       refs.find(_.range.contains(pos))
 
 
@@ -80,26 +84,23 @@
 
     def accumulate(message: XML.Tree): Command.State =
       message match {
-        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
-          copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
+        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
 
         case XML.Elem(Markup(Markup.REPORT, _), elems) =>
           (this /: elems)((state, elem) =>
             elem match {
               case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
                 atts match {
-                  case Position.Range(begin, end) =>
+                  case Position.Range(range) =>
                     if (kind == Markup.ML_TYPING) {
                       val info = Pretty.string_of(body, margin = 40)
-                      state.add_markup(
-                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+                      state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
                     }
                     else if (kind == Markup.ML_REF) {
                       body match {
                         case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
                           state.add_markup(
-                            command.markup_node(
-                              begin - 1, end - 1,
+                            command.decode_range(range,
                               Command.RefInfo(
                                 Position.get_file(props),
                                 Position.get_line(props),
@@ -110,7 +111,7 @@
                     }
                     else {
                       state.add_markup(
-                        command.markup_node(begin - 1, end - 1,
+                        command.decode_range(range,
                           Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
                     }
                   case _ => state
@@ -151,21 +152,18 @@
   val source: String = span.map(_.source).mkString
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   def length: Int = source.length
+  val range: Text.Range = Text.Range(0, length)
 
   lazy val symbol_index = new Symbol.Index(source)
 
 
   /* markup */
 
-  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
-  {
-    val start = symbol_index.decode(begin)
-    val stop = symbol_index.decode(end)
-    new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
-  }
+  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
+    new Markup_Tree.Node(symbol_index.decode(range), info)
 
 
   /* accumulated results */
 
-  val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
+  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
 }
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/PIDE/isar_document.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -0,0 +1,42 @@
+(*  Title:      Pure/PIDE/isar_document.ML
+    Author:     Makarius
+
+Protocol commands for interactive Isar documents.
+*)
+
+structure Isar_Document: sig end =
+struct
+
+val global_state = Synchronized.var "Isar_Document" Document.init_state;
+val change_state = Synchronized.change global_state;
+
+val _ =
+  Isabelle_Process.add_command "Isar_Document.define_command"
+    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
+
+val _ =
+  Isabelle_Process.add_command "Isar_Document.edit_version"
+    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
+      let
+        val old_id = Document.parse_id old_id_string;
+        val new_id = Document.parse_id new_id_string;
+        val edits =
+          XML_Data.dest_list
+            (XML_Data.dest_pair
+              XML_Data.dest_string
+              (XML_Data.dest_option
+                (XML_Data.dest_list
+                  (XML_Data.dest_pair
+                    (XML_Data.dest_option XML_Data.dest_int)
+                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
+
+      val (updates, state') = Document.edit old_id new_id edits state;
+      val _ =
+        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
+        |> Markup.markup (Markup.assign new_id)
+        |> Output.status;
+      val state'' = Document.execute new_id state';
+    in state'' end));
+
+end;
+
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/PIDE/isar_document.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -0,0 +1,65 @@
+/*  Title:      Pure/PIDE/isar_document.scala
+    Author:     Makarius
+
+Protocol commands for interactive Isar documents.
+*/
+
+package isabelle
+
+
+object Isar_Document
+{
+  /* protocol messages */
+
+  object Assign {
+    def unapply(msg: XML.Tree)
+        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+      msg match {
+        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
+          val id_edits = edits.map(Edit.unapply)
+          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
+          else None
+        case _ => None
+      }
+  }
+
+  object Edit {
+    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
+      msg match {
+        case XML.Elem(
+          Markup(Markup.EDIT,
+            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+        case _ => None
+      }
+  }
+}
+
+
+trait Isar_Document extends Isabelle_Process
+{
+  import Isar_Document._
+
+
+  /* commands */
+
+  def define_command(id: Document.Command_ID, text: String): Unit =
+    input("Isar_Document.define_command", Document.ID(id), text)
+
+
+  /* document versions */
+
+  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
+      edits: List[Document.Edit[Document.Command_ID]])
+  {
+    val arg =
+      XML_Data.make_list(
+        XML_Data.make_pair(XML_Data.make_string)(
+          XML_Data.make_option(XML_Data.make_list(
+              XML_Data.make_pair(
+                XML_Data.make_option(XML_Data.make_long))(
+                XML_Data.make_option(XML_Data.make_long))))))(edits)
+
+    input("Isar_Document.edit_version",
+      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
+  }
+}
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/PIDE/markup_node.scala
--- a/src/Pure/PIDE/markup_node.scala	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-/*  Title:      Pure/PIDE/markup_node.scala
-    Author:     Fabian Immler, TU Munich
-    Author:     Makarius
-
-Text markup nodes.
-*/
-
-package isabelle
-
-
-import javax.swing.tree.DefaultMutableTreeNode
-
-
-
-case class Markup_Node(val range: Text.Range, val info: Any)
-{
-  def fits_into(that: Markup_Node): Boolean =
-    that.range.start <= this.range.start && this.range.stop <= that.range.stop
-}
-
-
-case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
-{
-  private def add(branch: Markup_Tree) =   // FIXME avoid sort
-    copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
-
-  private def remove(bs: List[Markup_Tree]) =
-    copy(branches = branches.filterNot(bs.contains(_)))
-
-  def + (new_tree: Markup_Tree): Markup_Tree =
-  {
-    val new_node = new_tree.node
-    if (new_node fits_into node) {
-      var inserted = false
-      val new_branches =
-        branches.map(branch =>
-          if ((new_node fits_into branch.node) && !inserted) {
-            inserted = true
-            branch + new_tree
-          }
-          else branch)
-      if (!inserted) {
-        // new_tree did not fit into children of this
-        // -> insert between this and its branches
-        val fitting = branches filter(_.node fits_into new_node)
-        (this remove fitting) add ((new_tree /: fitting)(_ + _))
-      }
-      else copy(branches = new_branches)
-    }
-    else {
-      System.err.println("Ignored nonfitting markup: " + new_node)
-      this
-    }
-  }
-
-  def flatten: List[Markup_Node] =
-  {
-    var next_x = node.range.start
-    if (branches.isEmpty) List(this.node)
-    else {
-      val filled_gaps =
-        for {
-          child <- branches
-          markups =
-            if (next_x < child.node.range.start)
-              new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
-            else child.flatten
-          update = (next_x = child.node.range.stop)
-          markup <- markups
-        } yield markup
-      if (next_x < node.range.stop)
-        filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
-      else filled_gaps
-    }
-  }
-}
-
-
-case class Markup_Text(val markup: List[Markup_Tree], val content: String)
-{
-  private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup)  // FIXME !?
-
-  def + (new_tree: Markup_Tree): Markup_Text =
-    new Markup_Text((root + new_tree).branches, content)
-
-  def filter(pred: Markup_Node => Boolean): Markup_Text =
-  {
-    def filt(tree: Markup_Tree): List[Markup_Tree] =
-    {
-      val branches = tree.branches.flatMap(filt(_))
-      if (pred(tree.node)) List(tree.copy(branches = branches))
-      else branches
-    }
-    new Markup_Text(markup.flatMap(filt(_)), content)
-  }
-
-  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
-
-  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
-  {
-    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
-    {
-      val node = swing_node(tree.node)
-      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
-      node
-    }
-    swing(root)
-  }
-}
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/PIDE/markup_tree.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -0,0 +1,144 @@
+/*  Title:      Pure/PIDE/markup_tree.scala
+    Author:     Fabian Immler, TU Munich
+    Author:     Makarius
+
+Markup trees over nested / non-overlapping text ranges.
+*/
+
+package isabelle
+
+
+import javax.swing.tree.DefaultMutableTreeNode
+
+import scala.collection.immutable.SortedMap
+import scala.collection.mutable
+import scala.annotation.tailrec
+
+
+object Markup_Tree
+{
+  case class Node(val range: Text.Range, val info: Any)
+  {
+    def contains(that: Node): Boolean = this.range contains that.range
+    def intersect(r: Text.Range): Node = Node(range.intersect(r), info)
+  }
+
+
+  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
+
+  object Branches
+  {
+    type Entry = (Node, Markup_Tree)
+    type T = SortedMap[Node, Entry]
+
+    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
+      {
+        def compare(x: Node, y: Node): Int = x.range compare y.range
+      })
+    def update(branches: T, entries: Entry*): T =
+      branches ++ entries.map(e => (e._1 -> e))
+  }
+
+  val empty = new Markup_Tree(Branches.empty)
+}
+
+
+case class Markup_Tree(val branches: Markup_Tree.Branches.T)
+{
+  import Markup_Tree._
+
+  def + (new_node: Node): Markup_Tree =
+  {
+    branches.get(new_node) match {
+      case None =>
+        new Markup_Tree(Branches.update(branches, new_node -> empty))
+      case Some((node, subtree)) =>
+        if (node.range != new_node.range && node.contains(new_node))
+          new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
+        else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
+          new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
+        else {
+          var overlapping = Branches.empty
+          var rest = branches
+          while (rest.isDefinedAt(new_node)) {
+            overlapping = Branches.update(overlapping, rest(new_node))
+            rest -= new_node
+          }
+          if (overlapping.forall(e => new_node.contains(e._1)))
+            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
+          else { // FIXME split markup!?
+            System.err.println("Ignored overlapping markup: " + new_node)
+            this
+          }
+        }
+    }
+  }
+
+  // FIXME depth-first with result markup stack
+  // FIXME projection to given range
+  def flatten(parent: Node): List[Node] =
+  {
+    val result = new mutable.ListBuffer[Node]
+    var offset = parent.range.start
+    for ((_, (node, subtree)) <- branches.iterator) {
+      if (offset < node.range.start)
+        result += new Node(Text.Range(offset, node.range.start), parent.info)
+      result ++= subtree.flatten(node)
+      offset = node.range.stop
+    }
+    if (offset < parent.range.stop)
+      result += new Node(Text.Range(offset, parent.range.stop), parent.info)
+    result.toList
+  }
+
+  def filter(pred: Node => Boolean): Markup_Tree =
+  {
+    val bs = branches.toList.flatMap(entry => {
+      val (_, (node, subtree)) = entry
+      if (pred(node)) List((node, (node, subtree.filter(pred))))
+      else subtree.filter(pred).branches.toList
+    })
+    new Markup_Tree(Branches.empty ++ bs)
+  }
+
+  def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
+  {
+    def stream(parent: Node, bs: Branches.T): Stream[Node] =
+    {
+      val start = Node(parent.range.start_range, Nil)
+      val stop = Node(parent.range.stop_range, Nil)
+      val substream =
+        (for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield {
+          if (sel.isDefinedAt(node))
+            stream(node.intersect(parent.range), subtree.branches)
+          else stream(parent, subtree.branches)
+        }).flatten
+
+      def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
+        s match {
+          case node #:: rest =>
+            if (last < node.range.start)
+              parent.intersect(Text.Range(last, node.range.start)) #::
+                node #:: padding(node.range.stop, rest)
+            else node #:: padding(node.range.stop, rest)
+          case Stream.Empty =>  // FIXME
+            if (last < parent.range.stop)
+            Stream(parent.intersect(Text.Range(last, parent.range.stop)))
+            else Stream.Empty
+        }
+      padding(parent.range.start, substream)
+    }
+    // FIXME handle disjoint range!?
+    stream(Node(range, Nil), branches)
+  }
+
+  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
+  {
+    for ((_, (node, subtree)) <- branches) {
+      val current = swing_node(node)
+      subtree.swing_tree(current)(swing_node)
+      parent.add(current)
+    }
+  }
+}
+
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -10,15 +10,42 @@
 
 object Text
 {
-  /* offset and range */
+  /* offset */
 
   type Offset = Int
 
+
+  /* range: interval with total quasi-ordering */
+
+  object Range
+  {
+    object Ordering extends scala.math.Ordering[Range]
+    {
+      override def compare(r1: Range, r2: Range): Int = r1 compare r2
+    }
+  }
+
   sealed case class Range(val start: Offset, val stop: Offset)
   {
-    def contains(i: Offset): Boolean = start <= i && i < stop
+    require(start <= stop)
+
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = map(_ + i)
+    def contains(i: Offset): Boolean = start <= i && i < stop
+    def contains(that: Range): Boolean =
+      this == that || this.contains(that.start) && that.stop <= this.stop
+    def overlaps(that: Range): Boolean =
+      this == that || this.contains(that.start) || that.contains(this.start)
+    def compare(that: Range): Int =
+      if (overlaps(that)) 0
+      else if (this.start < that.start) -1
+      else 1
+
+    def start_range: Range = Range(start, start)
+    def stop_range: Range = Range(stop, stop)
+
+    def intersect(that: Range): Range =
+      Range(this.start max that.start, this.stop min that.stop)
   }
 
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/ROOT.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -179,9 +179,9 @@
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
-if ml_system = "polyml-5.3.0"
-then use "ML/ml_compiler_polyml-5.3.ML"
-else use "ML/ml_compiler.ML";
+if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
+then use "ML/ml_compiler.ML"
+else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";
 
 (*theory sources*)
@@ -257,7 +257,7 @@
 
 use "System/session.ML";
 use "System/isabelle_process.ML";
-use "System/isar_document.ML";
+use "PIDE/isar_document.ML";
 use "System/isar.ML";
 
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -181,9 +181,9 @@
   | FloatSy     => Markup.numeral
   | XNumSy      => Markup.numeral
   | StrSy       => Markup.inner_string
-  | Space       => Markup.none
+  | Space       => Markup.empty
   | Comment     => Markup.inner_comment
-  | EOF         => Markup.none;
+  | EOF         => Markup.empty;
 
 fun report_token ctxt (Token (kind, _, (pos, _))) =
   Context_Position.report ctxt (token_kind_markup kind) pos;
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/System/isar_document.ML
--- a/src/Pure/System/isar_document.ML	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(*  Title:      Pure/System/isar_document.ML
-    Author:     Makarius
-
-Protocol commands for interactive Isar documents.
-*)
-
-structure Isar_Document: sig end =
-struct
-
-val global_state = Synchronized.var "Isar_Document" Document.init_state;
-val change_state = Synchronized.change global_state;
-
-val _ =
-  Isabelle_Process.add_command "Isar_Document.define_command"
-    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
-
-val _ =
-  Isabelle_Process.add_command "Isar_Document.edit_version"
-    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
-      let
-        val old_id = Document.parse_id old_id_string;
-        val new_id = Document.parse_id new_id_string;
-        val edits =
-          XML_Data.dest_list
-            (XML_Data.dest_pair
-              XML_Data.dest_string
-              (XML_Data.dest_option
-                (XML_Data.dest_list
-                  (XML_Data.dest_pair
-                    (XML_Data.dest_option XML_Data.dest_int)
-                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
-
-      val (updates, state') = Document.edit old_id new_id edits state;
-      val _ =
-        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
-        |> Markup.markup (Markup.assign new_id)
-        |> Output.status;
-      val state'' = Document.execute new_id state';
-    in state'' end));
-
-end;
-
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/System/isar_document.scala
--- a/src/Pure/System/isar_document.scala	Thu Aug 19 16:08:59 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-/*  Title:      Pure/System/isar_document.scala
-    Author:     Makarius
-
-Protocol commands for interactive Isar documents.
-*/
-
-package isabelle
-
-
-object Isar_Document
-{
-  /* protocol messages */
-
-  object Assign {
-    def unapply(msg: XML.Tree)
-        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
-      msg match {
-        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
-          val id_edits = edits.map(Edit.unapply)
-          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
-          else None
-        case _ => None
-      }
-  }
-
-  object Edit {
-    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
-      msg match {
-        case XML.Elem(
-          Markup(Markup.EDIT,
-            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
-        case _ => None
-      }
-  }
-}
-
-
-trait Isar_Document extends Isabelle_Process
-{
-  import Isar_Document._
-
-
-  /* commands */
-
-  def define_command(id: Document.Command_ID, text: String): Unit =
-    input("Isar_Document.define_command", Document.ID(id), text)
-
-
-  /* document versions */
-
-  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
-      edits: List[Document.Edit[Document.Command_ID]])
-  {
-    val arg =
-      XML_Data.make_list(
-        XML_Data.make_pair(XML_Data.make_string)(
-          XML_Data.make_option(XML_Data.make_list(
-              XML_Data.make_pair(
-                XML_Data.make_option(XML_Data.make_long))(
-                XML_Data.make_option(XML_Data.make_long))))))(edits)
-
-    input("Isar_Document.edit_version",
-      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
-  }
-}
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -59,9 +59,9 @@
   | Token.String        => Markup.string
   | Token.AltString     => Markup.altstring
   | Token.Verbatim      => Markup.verbatim
-  | Token.Space         => Markup.none
+  | Token.Space         => Markup.empty
   | Token.Comment       => Markup.comment
-  | Token.InternalValue => Markup.none
+  | Token.InternalValue => Markup.empty
   | Token.Malformed     => Markup.malformed
   | Token.Error _       => Markup.malformed
   | Token.Sync          => Markup.control
@@ -73,10 +73,8 @@
     let
       val kind = Token.kind_of tok;
       val props =
-        if kind = Token.Command then
-          (case Keyword.command_keyword (Token.content_of tok) of
-            SOME k => Markup.properties [(Markup.kindN, Keyword.kind_of k)]
-          | NONE => I)
+        if kind = Token.Command
+        then Markup.properties [(Markup.nameN, Token.content_of tok)]
         else I;
     in props (token_kind_markup kind) end;
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/build-jars	Thu Aug 19 17:41:52 2010 +0200
@@ -29,6 +29,7 @@
   General/position.scala
   General/pretty.scala
   General/scan.scala
+  General/sha1.scala
   General/symbol.scala
   General/xml.scala
   General/xml_data.scala
@@ -40,7 +41,8 @@
   Isar/token.scala
   PIDE/command.scala
   PIDE/document.scala
-  PIDE/markup_node.scala
+  PIDE/isar_document.scala
+  PIDE/markup_tree.scala
   PIDE/text.scala
   System/cygwin.scala
   System/download.scala
@@ -49,7 +51,6 @@
   System/isabelle_process.scala
   System/isabelle_syntax.scala
   System/isabelle_system.scala
-  System/isar_document.scala
   System/platform.scala
   System/session.scala
   System/session_manager.scala
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/context_position.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -9,6 +9,7 @@
   val is_visible: Proof.context -> bool
   val set_visible: bool -> Proof.context -> Proof.context
   val restore_visible: Proof.context -> Proof.context -> Proof.context
+  val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
   val report: Proof.context -> Markup.T -> Position.T -> unit
 end;
 
@@ -25,7 +26,9 @@
 val set_visible = Data.put;
 val restore_visible = set_visible o is_visible;
 
-fun report ctxt markup pos =
-  if is_visible ctxt then Position.report markup pos else ();
+fun report_text ctxt markup pos txt =
+  if is_visible ctxt then Position.report_text markup pos txt else ();
+
+fun report ctxt markup pos = report_text ctxt markup pos "";
 
 end;
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Pure/pure_setup.ML	Thu Aug 19 17:41:52 2010 +0200
@@ -18,8 +18,9 @@
 
 (* ML toplevel pretty printing *)
 
-if String.isPrefix "smlnj" ml_system then ()
-else toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
+if String.isPrefix "polyml" ml_system
+then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
+else ();
 
 toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
 toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
@@ -39,15 +40,10 @@
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
-if ml_system = "polyml-5.3.0"
-then use "ML/install_pp_polyml-5.3.ML"
-else if String.isPrefix "polyml" ml_system
+if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
 then use "ML/install_pp_polyml.ML"
-else ();
-
-if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
-  Secure.use_text ML_Parse.global_context (0, "") false
-    "PolyML.Compiler.maxInlineSize := 20"
+else if String.isPrefix "polyml" ml_system
+then use "ML/install_pp_polyml-5.3.ML"
 else ();
 
 
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -279,7 +279,7 @@
       for {
         (command, command_start) <-
           snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
-        markup <- snapshot.state(command).highlight.flatten
+        markup <- snapshot.state(command).highlight
         val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
         if (abs_stop > start)
         if (abs_start < stop)
diff -r 32ad17fe2b9c -r befdd6833ec0 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 19 16:08:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 19 17:41:52 2010 +0200
@@ -79,7 +79,7 @@
       case Some((word, cs)) =>
         val ds =
           (if (Isabelle_Encoding.is_active(buffer))
-            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
+            cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
            else cs).filter(_ != word)
         if (ds.isEmpty) null
         else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
@@ -129,7 +129,7 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
-      root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
+      snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) =>
           {
             val content = command.source(node.range).replace('\n', ' ')
             val id = command.id
@@ -146,7 +146,7 @@
               override def getEnd: Position = command_start + node.range.stop
               override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
             })
-          }))
+          })
     }
   }
 }