merged
authorwenzelm
Thu Aug 19 17:41:52 2010 +0200 (2010-08-19)
changeset 38559befdd6833ec0
parent 38558 32ad17fe2b9c
parent 38486 f5bbfc019937
child 38560 004c35739d75
merged
NEWS
lib/scripts/run-polyml-5.0
src/Pure/ML-Systems/compiler_polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/PIDE/markup_node.scala
src/Pure/System/isar_document.ML
src/Pure/System/isar_document.scala
     1.1 --- a/Admin/polyml/README	Thu Aug 19 16:08:59 2010 +0200
     1.2 +++ b/Admin/polyml/README	Thu Aug 19 17:41:52 2010 +0200
     1.3 @@ -1,27 +1,15 @@
     1.4 -
     1.5 -This distribution of Poly/ML 5.3 is based on the original
     1.6 -polyml.5.3.tar.gz from http://www.polyml.org with some minimal changes:
     1.7 +Poly/ML for Isabelle
     1.8 +====================
     1.9  
    1.10 -diff polyml.5.3/libpolyml/processes.cpp-orig polyml.5.3/libpolyml/processes.cpp
    1.11 -995,996c995,996
    1.12 -<     // we set this to 100ms so that we're not waiting too long.
    1.13 -<     if (maxMillisecs > 100) maxMillisecs = 100;
    1.14 ----
    1.15 ->     // we set this to 10ms so that we're not waiting too long.
    1.16 ->     if (maxMillisecs > 10) maxMillisecs = 10;
    1.17 +This distribution of Poly/ML 5.4 has been compiled from the original
    1.18 +sources using the included build script.  For example:
    1.19  
    1.20 -
    1.21 -Then it is compiled as follows:
    1.22 +  ./build polyml.5.4 x86-linux --with-gmp
    1.23  
    1.24 -  cd polyml.5.3
    1.25 -  ./configure --prefix="$HOME/tmp/polyml"
    1.26 -  make
    1.27 -  make install
    1.28 -
    1.29 -
    1.30 -Now $HOME/tmp/polyml/bin/* and $HOME/tmp/polyml/lib/* are moved to the
    1.31 -platform-specific target directory (e.g. polyml-5.3.0/x86-linux).
    1.32 +The resulting executables and shared libraries are moved to
    1.33 +x86-linux/.  This directory layout accomodates the standard ML_HOME
    1.34 +settings for Isabelle.
    1.35  
    1.36  
    1.37  	Makarius
    1.38 -	26-May-2010
    1.39 +	17-Aug-2010
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/Admin/polyml/build	Thu Aug 19 17:41:52 2010 +0200
     2.3 @@ -0,0 +1,85 @@
     2.4 +#!/usr/bin/env bash
     2.5 +#
     2.6 +# Multi-platform build script for Poly/ML
     2.7 +
     2.8 +THIS="$(cd "$(dirname "$0")"; pwd)"
     2.9 +PRG="$(basename "$0")"
    2.10 +
    2.11 +
    2.12 +# diagnostics
    2.13 +
    2.14 +function usage()
    2.15 +{
    2.16 +  echo
    2.17 +  echo "Usage: $PRG SOURCE TARGET [OPTIONS]"
    2.18 +  echo
    2.19 +  echo "  Build Poly/ML in SOURCE directory for given platform in TARGET,"
    2.20 +  echo "  using the usual Isabelle platform identifiers."
    2.21 +  echo
    2.22 +  echo "  Additional options for ./configure may be given, e.g. --with-gmp"
    2.23 +  echo
    2.24 +  exit 1
    2.25 +}
    2.26 +
    2.27 +function fail()
    2.28 +{
    2.29 +  echo "$1" >&2
    2.30 +  exit 2
    2.31 +}
    2.32 +
    2.33 +
    2.34 +# command line args
    2.35 +
    2.36 +[ "$#" -eq 0 ] && usage
    2.37 +SOURCE="$1"; shift
    2.38 +
    2.39 +[ "$#" -eq 0 ] && usage
    2.40 +TARGET="$1"; shift
    2.41 +
    2.42 +USER_OPTIONS=("$@")
    2.43 +
    2.44 +
    2.45 +# main
    2.46 +
    2.47 +[ -d "$SOURCE" ] || fail "Bad source directory: \"$SOURCE\""
    2.48 +
    2.49 +case "$TARGET" in
    2.50 +  x86-linux)
    2.51 +    OPTIONS=()
    2.52 +    ;;
    2.53 +  x86_64-linux)
    2.54 +    OPTIONS=()
    2.55 +    ;;
    2.56 +  x86-darwin)
    2.57 +    OPTIONS=(--build=i686-darwin CFLAGS='-arch i686 -O3'
    2.58 +      CXXFLAGS='-arch i686 -O3' CCASFLAGS='-arch i686 -O3')
    2.59 +    ;;
    2.60 +  x86_64-darwin)
    2.61 +    OPTIONS=(--build=x86_64-darwin CFLAGS='-arch x86_64 -O3'
    2.62 +      CXXFLAGS='-arch x86_64 -O3' CCASFLAGS='-arch x86_64')
    2.63 +    ;;
    2.64 +  x86-cygwin)
    2.65 +    OPTIONS=()
    2.66 +    ;;
    2.67 +  ppc-darwin | sparc-solaris | x86-solaris | x86-bsd)
    2.68 +    OPTIONS=()
    2.69 +    ;;
    2.70 +  *)
    2.71 +    fail "Bad platform identifier: \"$TARGET\""
    2.72 +    ;;
    2.73 +esac
    2.74 +
    2.75 +(
    2.76 +  cd "$SOURCE"
    2.77 +  make distclean
    2.78 +
    2.79 +  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
    2.80 +    make compiler && \
    2.81 +    make install; } || fail "Build failed"
    2.82 +)
    2.83 +
    2.84 +mkdir -p "$TARGET"
    2.85 +mv "$SOURCE/$TARGET/bin/"* "$TARGET/"
    2.86 +mv "$SOURCE/$TARGET/lib/"* "$TARGET/"
    2.87 +rmdir "$SOURCE/$TARGET/bin" "$SOURCE/$TARGET/lib"
    2.88 +rm -rf "$SOURCE/$TARGET/share"
     3.1 --- a/NEWS	Thu Aug 19 16:08:59 2010 +0200
     3.2 +++ b/NEWS	Thu Aug 19 17:41:52 2010 +0200
     3.3 @@ -172,6 +172,11 @@
     3.4  change in semantics.
     3.5  
     3.6  
     3.7 +*** System ***
     3.8 +
     3.9 +* Discontinued support for Poly/ML 5.0 and 5.1 versions.
    3.10 +
    3.11 +
    3.12  
    3.13  New in Isabelle2009-2 (June 2010)
    3.14  ---------------------------------
     4.1 --- a/README	Thu Aug 19 16:08:59 2010 +0200
     4.2 +++ b/README	Thu Aug 19 17:41:52 2010 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4     Windows with Cygwin, Mac OS) and depends on the following main
     4.5     add-on tools:
     4.6  
     4.7 -     * The Poly/ML compiler and runtime system (version 5.x).
     4.8 +     * The Poly/ML compiler and runtime system (version 5.2.1 or later).
     4.9       * The GNU bash shell (version 3.x or 2.x).
    4.10       * Perl (version 5.x).
    4.11       * GNU Emacs (version 22) -- for the Proof General interface.
     5.1 --- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Aug 19 16:08:59 2010 +0200
     5.2 +++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Thu Aug 19 17:41:52 2010 +0200
     5.3 @@ -97,7 +97,7 @@
     5.4  text %mlref {*
     5.5    \begin{mldecls}
     5.6    @{index_ML_type local_theory: Proof.context} \\
     5.7 -  @{index_ML Named_Target.init: "string option -> theory -> local_theory"} \\[1ex]
     5.8 +  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
     5.9    @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
    5.10      local_theory -> (term * (string * thm)) * local_theory"} \\
    5.11    @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
    5.12 @@ -114,13 +114,13 @@
    5.13    with operations on expecting a regular @{text "ctxt:"}~@{ML_type
    5.14    Proof.context}.
    5.15  
    5.16 -  \item @{ML Named_Target.init}~@{text "NONE thy"} initializes a
    5.17 -  trivial local theory from the given background theory.
    5.18 -  Alternatively, @{text "SOME name"} may be given to initialize a
    5.19 -  @{command locale} or @{command class} context (a fully-qualified
    5.20 -  internal name is expected here).  This is useful for experimentation
    5.21 -  --- normally the Isar toplevel already takes care to initialize the
    5.22 -  local theory context.
    5.23 +  \item @{ML Named_Target.init}~@{text "name thy"} initializes a local
    5.24 +  theory derived from the given background theory.  An empty name
    5.25 +  refers to a \emph{global theory} context, and a non-empty name
    5.26 +  refers to a @{command locale} or @{command class} context (a
    5.27 +  fully-qualified internal name is expected here).  This is useful for
    5.28 +  experimentation --- normally the Isar toplevel already takes care to
    5.29 +  initialize the local theory context.
    5.30  
    5.31    \item @{ML Local_Theory.define}~@{text "((b, mx), (a, rhs))
    5.32    lthy"} defines a local entity according to the specification that is
     6.1 --- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Aug 19 16:08:59 2010 +0200
     6.2 +++ b/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Thu Aug 19 17:41:52 2010 +0200
     6.3 @@ -123,7 +123,7 @@
     6.4  \begin{isamarkuptext}%
     6.5  \begin{mldecls}
     6.6    \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
     6.7 -  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string option -> theory -> local_theory| \\[1ex]
     6.8 +  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex]
     6.9    \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
    6.10  \verb|    local_theory -> (term * (string * thm)) * local_theory| \\
    6.11    \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
    6.12 @@ -139,13 +139,13 @@
    6.13    any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
    6.14    with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
    6.15  
    6.16 -  \item \verb|Named_Target.init|~\isa{NONE\ thy} initializes a
    6.17 -  trivial local theory from the given background theory.
    6.18 -  Alternatively, \isa{SOME\ name} may be given to initialize a
    6.19 -  \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
    6.20 -  internal name is expected here).  This is useful for experimentation
    6.21 -  --- normally the Isar toplevel already takes care to initialize the
    6.22 -  local theory context.
    6.23 +  \item \verb|Named_Target.init|~\isa{name\ thy} initializes a local
    6.24 +  theory derived from the given background theory.  An empty name
    6.25 +  refers to a \emph{global theory} context, and a non-empty name
    6.26 +  refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a
    6.27 +  fully-qualified internal name is expected here).  This is useful for
    6.28 +  experimentation --- normally the Isar toplevel already takes care to
    6.29 +  initialize the local theory context.
    6.30  
    6.31    \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
    6.32    given relatively to the current \isa{lthy} context.  In
     7.1 --- a/etc/isar-keywords-ZF.el	Thu Aug 19 16:08:59 2010 +0200
     7.2 +++ b/etc/isar-keywords-ZF.el	Thu Aug 19 17:41:52 2010 +0200
     7.3 @@ -8,8 +8,6 @@
     7.4    '("\\."
     7.5      "\\.\\."
     7.6      "Isabelle\\.command"
     7.7 -    "Isar\\.define_command"
     7.8 -    "Isar\\.edit_document"
     7.9      "ML"
    7.10      "ML_command"
    7.11      "ML_prf"
    7.12 @@ -256,8 +254,6 @@
    7.13  
    7.14  (defconst isar-keywords-control
    7.15    '("Isabelle\\.command"
    7.16 -    "Isar\\.define_command"
    7.17 -    "Isar\\.edit_document"
    7.18      "ProofGeneral\\.inform_file_processed"
    7.19      "ProofGeneral\\.inform_file_retracted"
    7.20      "ProofGeneral\\.kill_proof"
     8.1 --- a/etc/isar-keywords.el	Thu Aug 19 16:08:59 2010 +0200
     8.2 +++ b/etc/isar-keywords.el	Thu Aug 19 17:41:52 2010 +0200
     8.3 @@ -8,8 +8,6 @@
     8.4    '("\\."
     8.5      "\\.\\."
     8.6      "Isabelle\\.command"
     8.7 -    "Isar\\.define_command"
     8.8 -    "Isar\\.edit_document"
     8.9      "ML"
    8.10      "ML_command"
    8.11      "ML_prf"
    8.12 @@ -320,8 +318,6 @@
    8.13  
    8.14  (defconst isar-keywords-control
    8.15    '("Isabelle\\.command"
    8.16 -    "Isar\\.define_command"
    8.17 -    "Isar\\.edit_document"
    8.18      "ProofGeneral\\.inform_file_processed"
    8.19      "ProofGeneral\\.inform_file_retracted"
    8.20      "ProofGeneral\\.kill_proof"
     9.1 --- a/lib/scripts/run-polyml-5.0	Thu Aug 19 16:08:59 2010 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,87 +0,0 @@
     9.4 -#!/usr/bin/env bash
     9.5 -#
     9.6 -# Author: Makarius
     9.7 -#
     9.8 -# Poly/ML 5.0 startup script.
     9.9 -
    9.10 -export -n INFILE OUTFILE MLTEXT TERMINATE NOWRITE
    9.11 -
    9.12 -
    9.13 -## diagnostics
    9.14 -
    9.15 -function fail_out()
    9.16 -{
    9.17 -  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    9.18 -  exit 2
    9.19 -}
    9.20 -
    9.21 -function check_file()
    9.22 -{
    9.23 -  if [ ! -f "$1" ]; then
    9.24 -    echo "Unable to locate $1" >&2
    9.25 -    echo "Please check your ML system settings!" >&2
    9.26 -    exit 2
    9.27 -  fi
    9.28 -}
    9.29 -
    9.30 -
    9.31 -## compiler executables and libraries
    9.32 -
    9.33 -POLY="$ML_HOME/poly"
    9.34 -check_file "$POLY"
    9.35 -
    9.36 -if [ "$(basename "$ML_HOME")" = bin ]; then
    9.37 -  POLYLIB="$(cd "$ML_HOME"; cd "$(pwd -P)"; cd ../lib; pwd)"
    9.38 -else
    9.39 -  POLYLIB="$ML_HOME"
    9.40 -fi
    9.41 -
    9.42 -export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
    9.43 -export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
    9.44 -
    9.45 -
    9.46 -## prepare databases
    9.47 -
    9.48 -if [ -z "$INFILE" ]; then
    9.49 -  PRG="$POLY"
    9.50 -  EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
    9.51 -else
    9.52 -  check_file "$INFILE"
    9.53 -  PRG="$INFILE"
    9.54 -  EXIT=""
    9.55 -fi
    9.56 -
    9.57 -if [ -z "$OUTFILE" ]; then
    9.58 -  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
    9.59 -else
    9.60 -  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
    9.61 -  [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
    9.62 -  rm -f "${OUTFILE}.o" || fail_out
    9.63 -fi
    9.64 -
    9.65 -
    9.66 -## run it!
    9.67 -
    9.68 -MLTEXT="$EXIT $COMMIT $MLTEXT"
    9.69 -MLEXIT="commit();"
    9.70 -
    9.71 -if [ -z "$TERMINATE" ]; then
    9.72 -  FEEDER_OPTS=""
    9.73 -else
    9.74 -  FEEDER_OPTS="-q"
    9.75 -fi
    9.76 -
    9.77 -"$ISABELLE_HOME/lib/scripts/feeder" -p -h "$MLTEXT" -t "$MLEXIT" $FEEDER_OPTS | \
    9.78 -  { read FPID; "$PRG" -q $ML_OPTIONS; RC="$?"; kill -HUP "$FPID"; exit "$RC"; }
    9.79 -RC="$?"
    9.80 -
    9.81 -if [ -n "$OUTFILE" ]; then
    9.82 -  if [ -e "${OUTFILE}.o" ]; then
    9.83 -    cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml $POLY_LINK_OPTIONS || fail_out
    9.84 -    rm -f "${OUTFILE}.o"
    9.85 -    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
    9.86 -  fi
    9.87 -  [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
    9.88 -fi
    9.89 -
    9.90 -exit "$RC"
    10.1 --- a/src/Pure/General/markup.ML	Thu Aug 19 16:08:59 2010 +0200
    10.2 +++ b/src/Pure/General/markup.ML	Thu Aug 19 17:41:52 2010 +0200
    10.3 @@ -9,8 +9,8 @@
    10.4    val parse_int: string -> int
    10.5    val print_int: int -> string
    10.6    type T = string * Properties.T
    10.7 -  val none: T
    10.8 -  val is_none: T -> bool
    10.9 +  val empty: T
   10.10 +  val is_empty: T -> bool
   10.11    val properties: Properties.T -> T -> T
   10.12    val nameN: string
   10.13    val name: string -> T -> T
   10.14 @@ -142,10 +142,10 @@
   10.15  
   10.16  type T = string * Properties.T;
   10.17  
   10.18 -val none = ("", []);
   10.19 +val empty = ("", []);
   10.20  
   10.21 -fun is_none ("", _) = true
   10.22 -  | is_none _ = false;
   10.23 +fun is_empty ("", _) = true
   10.24 +  | is_empty _ = false;
   10.25  
   10.26  
   10.27  fun properties more_props ((elem, props): T) =
   10.28 @@ -356,7 +356,7 @@
   10.29      the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
   10.30  end;
   10.31  
   10.32 -fun output m = if is_none m then no_output else #output (get_mode ()) m;
   10.33 +fun output m = if is_empty m then no_output else #output (get_mode ()) m;
   10.34  
   10.35  val enclose = output #-> Library.enclose;
   10.36  
    11.1 --- a/src/Pure/General/markup.scala	Thu Aug 19 16:08:59 2010 +0200
    11.2 +++ b/src/Pure/General/markup.scala	Thu Aug 19 17:41:52 2010 +0200
    11.3 @@ -48,6 +48,11 @@
    11.4    }
    11.5  
    11.6  
    11.7 +  /* empty */
    11.8 +
    11.9 +  val Empty = Markup("", Nil)
   11.10 +
   11.11 +
   11.12    /* name */
   11.13  
   11.14    val NAME = "name"
    12.1 --- a/src/Pure/General/position.scala	Thu Aug 19 16:08:59 2010 +0200
    12.2 +++ b/src/Pure/General/position.scala	Thu Aug 19 17:41:52 2010 +0200
    12.3 @@ -20,13 +20,13 @@
    12.4    def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
    12.5    def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos)
    12.6  
    12.7 -  def get_range(pos: T): Option[(Int, Int)] =
    12.8 +  def get_range(pos: T): Option[Text.Range] =
    12.9      (get_offset(pos), get_end_offset(pos)) match {
   12.10 -      case (Some(begin), Some(end)) => Some(begin, end)
   12.11 -      case (Some(begin), None) => Some(begin, begin + 1)
   12.12 +      case (Some(start), Some(stop)) => Some(Text.Range(start, stop))
   12.13 +      case (Some(start), None) => Some(Text.Range(start, start + 1))
   12.14        case (None, _) => None
   12.15      }
   12.16  
   12.17    object Id { def unapply(pos: T): Option[Long] = get_id(pos) }
   12.18 -  object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
   12.19 +  object Range { def unapply(pos: T): Option[Text.Range] = get_range(pos) }
   12.20  }
    13.1 --- a/src/Pure/General/pretty.ML	Thu Aug 19 16:08:59 2010 +0200
    13.2 +++ b/src/Pure/General/pretty.ML	Thu Aug 19 17:41:52 2010 +0200
    13.3 @@ -132,7 +132,7 @@
    13.4  
    13.5  fun markup_block m arg = block_markup (Markup.output m) arg;
    13.6  
    13.7 -val blk = markup_block Markup.none;
    13.8 +val blk = markup_block Markup.empty;
    13.9  fun block prts = blk (2, prts);
   13.10  val strs = block o breaks o map str;
   13.11  
   13.12 @@ -142,7 +142,7 @@
   13.13  fun command name = mark Markup.command (str name);
   13.14  
   13.15  fun markup_chunks m prts = markup m (fbreaks prts);
   13.16 -val chunks = markup_chunks Markup.none;
   13.17 +val chunks = markup_chunks Markup.empty;
   13.18  fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
   13.19  
   13.20  fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Pure/General/sha1.scala	Thu Aug 19 17:41:52 2010 +0200
    14.3 @@ -0,0 +1,28 @@
    14.4 +/*  Title:      Pure/General/sha1.scala
    14.5 +    Author:     Makarius
    14.6 +
    14.7 +Digesting strings according to SHA-1 (see RFC 3174).
    14.8 +*/
    14.9 +
   14.10 +package isabelle
   14.11 +
   14.12 +
   14.13 +import java.security.MessageDigest
   14.14 +
   14.15 +
   14.16 +object SHA1
   14.17 +{
   14.18 +  def digest_bytes(bytes: Array[Byte]): String =
   14.19 +  {
   14.20 +    val result = new StringBuilder
   14.21 +    for (b <- MessageDigest.getInstance("SHA").digest(bytes)) {
   14.22 +      val i = b.asInstanceOf[Int] & 0xFF
   14.23 +      if (i < 16) result += '0'
   14.24 +      result ++= Integer.toHexString(i)
   14.25 +    }
   14.26 +    result.toString
   14.27 +  }
   14.28 +
   14.29 +  def digest(s: String): String = digest_bytes(Standard_System.string_bytes(s))
   14.30 +}
   14.31 +
    15.1 --- a/src/Pure/General/symbol.scala	Thu Aug 19 16:08:59 2010 +0200
    15.2 +++ b/src/Pure/General/symbol.scala	Thu Aug 19 17:41:52 2010 +0200
    15.3 @@ -106,8 +106,9 @@
    15.4        }
    15.5        buf.toArray
    15.6      }
    15.7 -    def decode(sym: Int): Int =
    15.8 +    def decode(sym1: Int): Int =
    15.9      {
   15.10 +      val sym = sym1 - 1
   15.11        val end = index.length
   15.12        def bisect(a: Int, b: Int): Int =
   15.13        {
   15.14 @@ -123,6 +124,7 @@
   15.15        if (i < 0) sym
   15.16        else index(i).chr + sym - index(i).sym
   15.17      }
   15.18 +    def decode(range: Text.Range): Text.Range = range.map(decode(_))
   15.19    }
   15.20  
   15.21  
    16.1 --- a/src/Pure/General/xml.ML	Thu Aug 19 16:08:59 2010 +0200
    16.2 +++ b/src/Pure/General/xml.ML	Thu Aug 19 17:41:52 2010 +0200
    16.3 @@ -79,7 +79,7 @@
    16.4    end;
    16.5  
    16.6  fun output_markup (markup as (name, atts)) =
    16.7 -  if Markup.is_none markup then Markup.no_output
    16.8 +  if Markup.is_empty markup then Markup.no_output
    16.9    else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
   16.10  
   16.11  
    17.1 --- a/src/Pure/General/xml.scala	Thu Aug 19 16:08:59 2010 +0200
    17.2 +++ b/src/Pure/General/xml.scala	Thu Aug 19 17:41:52 2010 +0200
    17.3 @@ -67,30 +67,15 @@
    17.4    def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
    17.5  
    17.6  
    17.7 -  /* iterate over content */
    17.8 -
    17.9 -  private type State = Option[(String, List[Tree])]
   17.10 +  /* text content */
   17.11  
   17.12 -  private def get_next(tree: Tree): State = tree match {
   17.13 -    case Elem(_, body) => get_nexts(body)
   17.14 -    case Text(content) => Some(content, Nil)
   17.15 -  }
   17.16 -  private def get_nexts(trees: List[Tree]): State = trees match {
   17.17 -    case Nil => None
   17.18 -    case t :: ts => get_next(t) match {
   17.19 -      case None => get_nexts(ts)
   17.20 -      case Some((s, r)) => Some((s, r ++ ts))
   17.21 +  def content_stream(tree: Tree): Stream[String] =
   17.22 +    tree match {
   17.23 +      case Elem(_, body) => body.toStream.flatten(content_stream(_))
   17.24 +      case Text(content) => Stream(content)
   17.25      }
   17.26 -  }
   17.27  
   17.28 -  def content(tree: Tree) = new Iterator[String] {
   17.29 -    private var state = get_next(tree)
   17.30 -    def hasNext() = state.isDefined
   17.31 -    def next() = state match {
   17.32 -      case Some((s, rest)) => { state = get_nexts(rest); s }
   17.33 -      case None => throw new NoSuchElementException("next on empty iterator")
   17.34 -    }
   17.35 -  }
   17.36 +  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
   17.37  
   17.38  
   17.39    /* pipe-lined cache for partial sharing */
    18.1 --- a/src/Pure/General/yxml.ML	Thu Aug 19 16:08:59 2010 +0200
    18.2 +++ b/src/Pure/General/yxml.ML	Thu Aug 19 17:41:52 2010 +0200
    18.3 @@ -52,7 +52,7 @@
    18.4  (* output *)
    18.5  
    18.6  fun output_markup (markup as (name, atts)) =
    18.7 -  if Markup.is_none markup then Markup.no_output
    18.8 +  if Markup.is_empty markup then Markup.no_output
    18.9    else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
   18.10  
   18.11  fun element name atts body =
    19.1 --- a/src/Pure/General/yxml.scala	Thu Aug 19 16:08:59 2010 +0200
    19.2 +++ b/src/Pure/General/yxml.scala	Thu Aug 19 17:41:52 2010 +0200
    19.3 @@ -85,7 +85,7 @@
    19.4      /* stack operations */
    19.5  
    19.6      def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
    19.7 -    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
    19.8 +    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup.Empty, buffer()))
    19.9  
   19.10      def add(x: XML.Tree)
   19.11      {
   19.12 @@ -101,7 +101,7 @@
   19.13      def pop()
   19.14      {
   19.15        (stack: @unchecked) match {
   19.16 -        case ((Markup("", _), _) :: _) => err_unbalanced("")
   19.17 +        case ((Markup.Empty, _) :: _) => err_unbalanced("")
   19.18          case ((markup, body) :: pending) =>
   19.19            stack = pending
   19.20            add(XML.Elem(markup, body.toList))
   19.21 @@ -122,7 +122,7 @@
   19.22        }
   19.23      }
   19.24      stack match {
   19.25 -      case List((Markup("", _), body)) => body.toList
   19.26 +      case List((Markup.Empty, body)) => body.toList
   19.27        case (Markup(name, _), _) :: _ => err_unbalanced(name)
   19.28      }
   19.29    }
    20.1 --- a/src/Pure/IsaMakefile	Thu Aug 19 16:08:59 2010 +0200
    20.2 +++ b/src/Pure/IsaMakefile	Thu Aug 19 17:41:52 2010 +0200
    20.3 @@ -21,7 +21,6 @@
    20.4  
    20.5  BOOTSTRAP_FILES = 					\
    20.6    ML-Systems/bash.ML 					\
    20.7 -  ML-Systems/compiler_polyml-5.0.ML			\
    20.8    ML-Systems/compiler_polyml-5.2.ML			\
    20.9    ML-Systems/compiler_polyml-5.3.ML			\
   20.10    ML-Systems/ml_name_space.ML				\
   20.11 @@ -29,8 +28,6 @@
   20.12    ML-Systems/multithreading.ML				\
   20.13    ML-Systems/multithreading_polyml.ML			\
   20.14    ML-Systems/overloading_smlnj.ML			\
   20.15 -  ML-Systems/polyml-5.0.ML				\
   20.16 -  ML-Systems/polyml-5.1.ML				\
   20.17    ML-Systems/polyml-5.2.1.ML				\
   20.18    ML-Systems/polyml-5.2.ML				\
   20.19    ML-Systems/polyml.ML					\
   20.20 @@ -160,6 +157,7 @@
   20.21    ML/ml_syntax.ML					\
   20.22    ML/ml_thms.ML						\
   20.23    PIDE/document.ML					\
   20.24 +  PIDE/isar_document.ML					\
   20.25    Proof/extraction.ML					\
   20.26    Proof/proof_rewrite_rules.ML				\
   20.27    Proof/proof_syntax.ML					\
   20.28 @@ -191,7 +189,6 @@
   20.29    Syntax/type_ext.ML					\
   20.30    System/isabelle_process.ML				\
   20.31    System/isar.ML					\
   20.32 -  System/isar_document.ML				\
   20.33    System/session.ML					\
   20.34    Thy/html.ML						\
   20.35    Thy/latex.ML						\
    21.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Aug 19 16:08:59 2010 +0200
    21.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Aug 19 17:41:52 2010 +0200
    21.3 @@ -16,6 +16,8 @@
    21.4    protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
    21.5    lazy val completion: Completion = new Completion + symbols  // FIXME !?
    21.6  
    21.7 +  def keyword_kind(name: String): Option[String] = keywords.get(name)
    21.8 +
    21.9    def + (name: String, kind: String): Outer_Syntax =
   21.10    {
   21.11      val new_keywords = keywords + (name -> kind)
    22.1 --- a/src/Pure/Isar/toplevel.scala	Thu Aug 19 16:08:59 2010 +0200
    22.2 +++ b/src/Pure/Isar/toplevel.scala	Thu Aug 19 17:41:52 2010 +0200
    22.3 @@ -15,16 +15,18 @@
    22.4    case object Finished extends Status
    22.5    case object Failed extends Status
    22.6  
    22.7 -  def command_status(markup: List[Markup]): Status =
    22.8 +  def command_status(markup: XML.Body): Status =
    22.9    {
   22.10      val forks = (0 /: markup) {
   22.11 -      case (i, Markup(Markup.FORKED, _)) => i + 1
   22.12 -      case (i, Markup(Markup.JOINED, _)) => i - 1
   22.13 +      case (i, XML.Elem(Markup(Markup.FORKED, _), _)) => i + 1
   22.14 +      case (i, XML.Elem(Markup(Markup.JOINED, _), _)) => i - 1
   22.15        case (i, _) => i
   22.16      }
   22.17      if (forks != 0) Forked(forks)
   22.18 -    else if (markup.exists(_.name == Markup.FAILED)) Failed
   22.19 -    else if (markup.exists(_.name == Markup.FINISHED)) Finished
   22.20 +    else if (markup.exists { case XML.Elem(Markup(Markup.FAILED, _), _) => true case _ => false })
   22.21 +      Failed
   22.22 +    else if (markup.exists { case XML.Elem(Markup(Markup.FINISHED, _), _) => true case _ => false })
   22.23 +      Finished
   22.24      else Unprocessed
   22.25    }
   22.26  }
    23.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Thu Aug 19 16:08:59 2010 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,32 +0,0 @@
    23.4 -(*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
    23.5 -
    23.6 -Runtime compilation for Poly/ML 5.0 and 5.1.
    23.7 -*)
    23.8 -
    23.9 -fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
   23.10 -  let
   23.11 -    val in_buffer = Unsynchronized.ref (explode (tune_source txt));
   23.12 -    val out_buffer = Unsynchronized.ref ([]: string list);
   23.13 -    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
   23.14 -
   23.15 -    val current_line = Unsynchronized.ref line;
   23.16 -    fun get () =
   23.17 -      (case ! in_buffer of
   23.18 -        [] => ""
   23.19 -      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
   23.20 -    fun put s = out_buffer := s :: ! out_buffer;
   23.21 -
   23.22 -    fun exec () =
   23.23 -      (case ! in_buffer of
   23.24 -        [] => ()
   23.25 -      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
   23.26 -  in
   23.27 -    exec () handle exn => (error (output ()); reraise exn);
   23.28 -    if verbose then print (output ()) else ()
   23.29 -  end;
   23.30 -
   23.31 -fun use_file context verbose name =
   23.32 -  let
   23.33 -    val instream = TextIO.openIn name;
   23.34 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   23.35 -  in use_text context (1, name) verbose txt end;
    24.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Aug 19 16:08:59 2010 +0200
    24.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu Aug 19 17:41:52 2010 +0200
    24.3 @@ -1,6 +1,6 @@
    24.4  (*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
    24.5  
    24.6 -Runtime compilation for Poly/ML 5.3.0.
    24.7 +Runtime compilation for Poly/ML 5.3 and 5.4.
    24.8  *)
    24.9  
   24.10  local
    25.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Aug 19 16:08:59 2010 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,19 +0,0 @@
    25.4 -(*  Title:      Pure/ML-Systems/polyml-5.0.ML
    25.5 -
    25.6 -Compatibility wrapper for Poly/ML 5.0.
    25.7 -*)
    25.8 -
    25.9 -fun reraise exn = raise exn;
   25.10 -
   25.11 -use "ML-Systems/unsynchronized.ML";
   25.12 -use "ML-Systems/universal.ML";
   25.13 -use "ML-Systems/thread_dummy.ML";
   25.14 -use "ML-Systems/ml_name_space.ML";
   25.15 -use "ML-Systems/polyml_common.ML";
   25.16 -use "ML-Systems/compiler_polyml-5.0.ML";
   25.17 -use "ML-Systems/pp_polyml.ML";
   25.18 -
   25.19 -val pointer_eq = PolyML.pointerEq;
   25.20 -
   25.21 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   25.22 -
    26.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Thu Aug 19 16:08:59 2010 +0200
    26.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.3 @@ -1,18 +0,0 @@
    26.4 -(*  Title:      Pure/ML-Systems/polyml-5.1.ML
    26.5 -
    26.6 -Compatibility wrapper for Poly/ML 5.1.
    26.7 -*)
    26.8 -
    26.9 -fun reraise exn = raise exn;
   26.10 -
   26.11 -use "ML-Systems/unsynchronized.ML";
   26.12 -use "ML-Systems/thread_dummy.ML";
   26.13 -use "ML-Systems/ml_name_space.ML";
   26.14 -use "ML-Systems/polyml_common.ML";
   26.15 -use "ML-Systems/compiler_polyml-5.0.ML";
   26.16 -use "ML-Systems/pp_polyml.ML";
   26.17 -
   26.18 -val pointer_eq = PolyML.pointerEq;
   26.19 -
   26.20 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   26.21 -
    27.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Aug 19 16:08:59 2010 +0200
    27.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Aug 19 17:41:52 2010 +0200
    27.3 @@ -1,6 +1,6 @@
    27.4  (*  Title:      Pure/ML-Systems/polyml.ML
    27.5  
    27.6 -Compatibility wrapper for Poly/ML 5.3.0.
    27.7 +Compatibility wrapper for Poly/ML 5.3 and 5.4.
    27.8  *)
    27.9  
   27.10  use "ML-Systems/unsynchronized.ML";
    28.1 --- a/src/Pure/ML/ml_lex.ML	Thu Aug 19 16:08:59 2010 +0200
    28.2 +++ b/src/Pure/ML/ml_lex.ML	Thu Aug 19 17:41:52 2010 +0200
    28.3 @@ -100,10 +100,10 @@
    28.4    | Real      => Markup.ML_numeral
    28.5    | Char      => Markup.ML_char
    28.6    | String    => Markup.ML_string
    28.7 -  | Space     => Markup.none
    28.8 +  | Space     => Markup.empty
    28.9    | Comment   => Markup.ML_comment
   28.10    | Error _   => Markup.ML_malformed
   28.11 -  | EOF       => Markup.none;
   28.12 +  | EOF       => Markup.empty;
   28.13  
   28.14  fun token_markup kind x =
   28.15    if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x
    29.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 19 16:08:59 2010 +0200
    29.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 19 17:41:52 2010 +0200
    29.3 @@ -27,9 +27,9 @@
    29.4  
    29.5    case class State(
    29.6      val command: Command,
    29.7 -    val status: List[Markup],
    29.8 +    val status: List[XML.Tree],
    29.9      val reverse_results: List[XML.Tree],
   29.10 -    val markup: Markup_Text)
   29.11 +    val markup: Markup_Tree)
   29.12    {
   29.13      /* content */
   29.14  
   29.15 @@ -37,23 +37,27 @@
   29.16  
   29.17      def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results)
   29.18  
   29.19 -    def add_markup(node: Markup_Tree): State = copy(markup = markup + node)
   29.20 +    def add_markup(node: Markup_Tree.Node): State = copy(markup = markup + node)
   29.21 +
   29.22 +    def markup_root_node: Markup_Tree.Node =
   29.23 +      new Markup_Tree.Node(command.range, XML.Elem(Markup(Markup.STATUS, Nil), status))
   29.24 +    def markup_root: Markup_Tree = markup + markup_root_node
   29.25  
   29.26  
   29.27      /* markup */
   29.28  
   29.29 -    lazy val highlight: Markup_Text =
   29.30 +    lazy val highlight: List[Markup_Tree.Node] =
   29.31      {
   29.32        markup.filter(_.info match {
   29.33          case Command.HighlightInfo(_, _) => true
   29.34          case _ => false
   29.35 -      })
   29.36 +      }).flatten(markup_root_node)
   29.37      }
   29.38  
   29.39 -    private lazy val types: List[Markup_Node] =
   29.40 +    private lazy val types: List[Markup_Tree.Node] =
   29.41        markup.filter(_.info match {
   29.42          case Command.TypeInfo(_) => true
   29.43 -        case _ => false }).flatten
   29.44 +        case _ => false }).flatten(markup_root_node)
   29.45  
   29.46      def type_at(pos: Text.Offset): Option[String] =
   29.47      {
   29.48 @@ -67,12 +71,12 @@
   29.49        }
   29.50      }
   29.51  
   29.52 -    private lazy val refs: List[Markup_Node] =
   29.53 +    private lazy val refs: List[Markup_Tree.Node] =
   29.54        markup.filter(_.info match {
   29.55          case Command.RefInfo(_, _, _, _) => true
   29.56 -        case _ => false }).flatten
   29.57 +        case _ => false }).flatten(markup_root_node)
   29.58  
   29.59 -    def ref_at(pos: Text.Offset): Option[Markup_Node] =
   29.60 +    def ref_at(pos: Text.Offset): Option[Markup_Tree.Node] =
   29.61        refs.find(_.range.contains(pos))
   29.62  
   29.63  
   29.64 @@ -80,26 +84,23 @@
   29.65  
   29.66      def accumulate(message: XML.Tree): Command.State =
   29.67        message match {
   29.68 -        case XML.Elem(Markup(Markup.STATUS, _), elems) =>
   29.69 -          copy(status = (for (XML.Elem(markup, _) <- elems) yield markup) ::: status)
   29.70 +        case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
   29.71  
   29.72          case XML.Elem(Markup(Markup.REPORT, _), elems) =>
   29.73            (this /: elems)((state, elem) =>
   29.74              elem match {
   29.75                case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
   29.76                  atts match {
   29.77 -                  case Position.Range(begin, end) =>
   29.78 +                  case Position.Range(range) =>
   29.79                      if (kind == Markup.ML_TYPING) {
   29.80                        val info = Pretty.string_of(body, margin = 40)
   29.81 -                      state.add_markup(
   29.82 -                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
   29.83 +                      state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
   29.84                      }
   29.85                      else if (kind == Markup.ML_REF) {
   29.86                        body match {
   29.87                          case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
   29.88                            state.add_markup(
   29.89 -                            command.markup_node(
   29.90 -                              begin - 1, end - 1,
   29.91 +                            command.decode_range(range,
   29.92                                Command.RefInfo(
   29.93                                  Position.get_file(props),
   29.94                                  Position.get_line(props),
   29.95 @@ -110,7 +111,7 @@
   29.96                      }
   29.97                      else {
   29.98                        state.add_markup(
   29.99 -                        command.markup_node(begin - 1, end - 1,
  29.100 +                        command.decode_range(range,
  29.101                            Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
  29.102                      }
  29.103                    case _ => state
  29.104 @@ -151,21 +152,18 @@
  29.105    val source: String = span.map(_.source).mkString
  29.106    def source(range: Text.Range): String = source.substring(range.start, range.stop)
  29.107    def length: Int = source.length
  29.108 +  val range: Text.Range = Text.Range(0, length)
  29.109  
  29.110    lazy val symbol_index = new Symbol.Index(source)
  29.111  
  29.112  
  29.113    /* markup */
  29.114  
  29.115 -  def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
  29.116 -  {
  29.117 -    val start = symbol_index.decode(begin)
  29.118 -    val stop = symbol_index.decode(end)
  29.119 -    new Markup_Tree(new Markup_Node(Text.Range(start, stop), info), Nil)
  29.120 -  }
  29.121 +  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node =
  29.122 +    new Markup_Tree.Node(symbol_index.decode(range), info)
  29.123  
  29.124  
  29.125    /* accumulated results */
  29.126  
  29.127 -  val empty_state: Command.State = Command.State(this, Nil, Nil, new Markup_Text(Nil, source))
  29.128 +  val empty_state: Command.State = Command.State(this, Nil, Nil, Markup_Tree.empty)
  29.129  }
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/Pure/PIDE/isar_document.ML	Thu Aug 19 17:41:52 2010 +0200
    30.3 @@ -0,0 +1,42 @@
    30.4 +(*  Title:      Pure/PIDE/isar_document.ML
    30.5 +    Author:     Makarius
    30.6 +
    30.7 +Protocol commands for interactive Isar documents.
    30.8 +*)
    30.9 +
   30.10 +structure Isar_Document: sig end =
   30.11 +struct
   30.12 +
   30.13 +val global_state = Synchronized.var "Isar_Document" Document.init_state;
   30.14 +val change_state = Synchronized.change global_state;
   30.15 +
   30.16 +val _ =
   30.17 +  Isabelle_Process.add_command "Isar_Document.define_command"
   30.18 +    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
   30.19 +
   30.20 +val _ =
   30.21 +  Isabelle_Process.add_command "Isar_Document.edit_version"
   30.22 +    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
   30.23 +      let
   30.24 +        val old_id = Document.parse_id old_id_string;
   30.25 +        val new_id = Document.parse_id new_id_string;
   30.26 +        val edits =
   30.27 +          XML_Data.dest_list
   30.28 +            (XML_Data.dest_pair
   30.29 +              XML_Data.dest_string
   30.30 +              (XML_Data.dest_option
   30.31 +                (XML_Data.dest_list
   30.32 +                  (XML_Data.dest_pair
   30.33 +                    (XML_Data.dest_option XML_Data.dest_int)
   30.34 +                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
   30.35 +
   30.36 +      val (updates, state') = Document.edit old_id new_id edits state;
   30.37 +      val _ =
   30.38 +        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
   30.39 +        |> Markup.markup (Markup.assign new_id)
   30.40 +        |> Output.status;
   30.41 +      val state'' = Document.execute new_id state';
   30.42 +    in state'' end));
   30.43 +
   30.44 +end;
   30.45 +
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 19 17:41:52 2010 +0200
    31.3 @@ -0,0 +1,65 @@
    31.4 +/*  Title:      Pure/PIDE/isar_document.scala
    31.5 +    Author:     Makarius
    31.6 +
    31.7 +Protocol commands for interactive Isar documents.
    31.8 +*/
    31.9 +
   31.10 +package isabelle
   31.11 +
   31.12 +
   31.13 +object Isar_Document
   31.14 +{
   31.15 +  /* protocol messages */
   31.16 +
   31.17 +  object Assign {
   31.18 +    def unapply(msg: XML.Tree)
   31.19 +        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
   31.20 +      msg match {
   31.21 +        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
   31.22 +          val id_edits = edits.map(Edit.unapply)
   31.23 +          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
   31.24 +          else None
   31.25 +        case _ => None
   31.26 +      }
   31.27 +  }
   31.28 +
   31.29 +  object Edit {
   31.30 +    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
   31.31 +      msg match {
   31.32 +        case XML.Elem(
   31.33 +          Markup(Markup.EDIT,
   31.34 +            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
   31.35 +        case _ => None
   31.36 +      }
   31.37 +  }
   31.38 +}
   31.39 +
   31.40 +
   31.41 +trait Isar_Document extends Isabelle_Process
   31.42 +{
   31.43 +  import Isar_Document._
   31.44 +
   31.45 +
   31.46 +  /* commands */
   31.47 +
   31.48 +  def define_command(id: Document.Command_ID, text: String): Unit =
   31.49 +    input("Isar_Document.define_command", Document.ID(id), text)
   31.50 +
   31.51 +
   31.52 +  /* document versions */
   31.53 +
   31.54 +  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
   31.55 +      edits: List[Document.Edit[Document.Command_ID]])
   31.56 +  {
   31.57 +    val arg =
   31.58 +      XML_Data.make_list(
   31.59 +        XML_Data.make_pair(XML_Data.make_string)(
   31.60 +          XML_Data.make_option(XML_Data.make_list(
   31.61 +              XML_Data.make_pair(
   31.62 +                XML_Data.make_option(XML_Data.make_long))(
   31.63 +                XML_Data.make_option(XML_Data.make_long))))))(edits)
   31.64 +
   31.65 +    input("Isar_Document.edit_version",
   31.66 +      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
   31.67 +  }
   31.68 +}
    32.1 --- a/src/Pure/PIDE/markup_node.scala	Thu Aug 19 16:08:59 2010 +0200
    32.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.3 @@ -1,109 +0,0 @@
    32.4 -/*  Title:      Pure/PIDE/markup_node.scala
    32.5 -    Author:     Fabian Immler, TU Munich
    32.6 -    Author:     Makarius
    32.7 -
    32.8 -Text markup nodes.
    32.9 -*/
   32.10 -
   32.11 -package isabelle
   32.12 -
   32.13 -
   32.14 -import javax.swing.tree.DefaultMutableTreeNode
   32.15 -
   32.16 -
   32.17 -
   32.18 -case class Markup_Node(val range: Text.Range, val info: Any)
   32.19 -{
   32.20 -  def fits_into(that: Markup_Node): Boolean =
   32.21 -    that.range.start <= this.range.start && this.range.stop <= that.range.stop
   32.22 -}
   32.23 -
   32.24 -
   32.25 -case class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
   32.26 -{
   32.27 -  private def add(branch: Markup_Tree) =   // FIXME avoid sort
   32.28 -    copy(branches = (branch :: branches).sortWith((a, b) => a.node.range.start < b.node.range.start))
   32.29 -
   32.30 -  private def remove(bs: List[Markup_Tree]) =
   32.31 -    copy(branches = branches.filterNot(bs.contains(_)))
   32.32 -
   32.33 -  def + (new_tree: Markup_Tree): Markup_Tree =
   32.34 -  {
   32.35 -    val new_node = new_tree.node
   32.36 -    if (new_node fits_into node) {
   32.37 -      var inserted = false
   32.38 -      val new_branches =
   32.39 -        branches.map(branch =>
   32.40 -          if ((new_node fits_into branch.node) && !inserted) {
   32.41 -            inserted = true
   32.42 -            branch + new_tree
   32.43 -          }
   32.44 -          else branch)
   32.45 -      if (!inserted) {
   32.46 -        // new_tree did not fit into children of this
   32.47 -        // -> insert between this and its branches
   32.48 -        val fitting = branches filter(_.node fits_into new_node)
   32.49 -        (this remove fitting) add ((new_tree /: fitting)(_ + _))
   32.50 -      }
   32.51 -      else copy(branches = new_branches)
   32.52 -    }
   32.53 -    else {
   32.54 -      System.err.println("Ignored nonfitting markup: " + new_node)
   32.55 -      this
   32.56 -    }
   32.57 -  }
   32.58 -
   32.59 -  def flatten: List[Markup_Node] =
   32.60 -  {
   32.61 -    var next_x = node.range.start
   32.62 -    if (branches.isEmpty) List(this.node)
   32.63 -    else {
   32.64 -      val filled_gaps =
   32.65 -        for {
   32.66 -          child <- branches
   32.67 -          markups =
   32.68 -            if (next_x < child.node.range.start)
   32.69 -              new Markup_Node(Text.Range(next_x, child.node.range.start), node.info) :: child.flatten
   32.70 -            else child.flatten
   32.71 -          update = (next_x = child.node.range.stop)
   32.72 -          markup <- markups
   32.73 -        } yield markup
   32.74 -      if (next_x < node.range.stop)
   32.75 -        filled_gaps ::: List(new Markup_Node(Text.Range(next_x, node.range.stop), node.info))
   32.76 -      else filled_gaps
   32.77 -    }
   32.78 -  }
   32.79 -}
   32.80 -
   32.81 -
   32.82 -case class Markup_Text(val markup: List[Markup_Tree], val content: String)
   32.83 -{
   32.84 -  private val root = new Markup_Tree(new Markup_Node(Text.Range(0, content.length), None), markup)  // FIXME !?
   32.85 -
   32.86 -  def + (new_tree: Markup_Tree): Markup_Text =
   32.87 -    new Markup_Text((root + new_tree).branches, content)
   32.88 -
   32.89 -  def filter(pred: Markup_Node => Boolean): Markup_Text =
   32.90 -  {
   32.91 -    def filt(tree: Markup_Tree): List[Markup_Tree] =
   32.92 -    {
   32.93 -      val branches = tree.branches.flatMap(filt(_))
   32.94 -      if (pred(tree.node)) List(tree.copy(branches = branches))
   32.95 -      else branches
   32.96 -    }
   32.97 -    new Markup_Text(markup.flatMap(filt(_)), content)
   32.98 -  }
   32.99 -
  32.100 -  def flatten: List[Markup_Node] = markup.flatten(_.flatten)
  32.101 -
  32.102 -  def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
  32.103 -  {
  32.104 -    def swing(tree: Markup_Tree): DefaultMutableTreeNode =
  32.105 -    {
  32.106 -      val node = swing_node(tree.node)
  32.107 -      tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
  32.108 -      node
  32.109 -    }
  32.110 -    swing(root)
  32.111 -  }
  32.112 -}
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Aug 19 17:41:52 2010 +0200
    33.3 @@ -0,0 +1,144 @@
    33.4 +/*  Title:      Pure/PIDE/markup_tree.scala
    33.5 +    Author:     Fabian Immler, TU Munich
    33.6 +    Author:     Makarius
    33.7 +
    33.8 +Markup trees over nested / non-overlapping text ranges.
    33.9 +*/
   33.10 +
   33.11 +package isabelle
   33.12 +
   33.13 +
   33.14 +import javax.swing.tree.DefaultMutableTreeNode
   33.15 +
   33.16 +import scala.collection.immutable.SortedMap
   33.17 +import scala.collection.mutable
   33.18 +import scala.annotation.tailrec
   33.19 +
   33.20 +
   33.21 +object Markup_Tree
   33.22 +{
   33.23 +  case class Node(val range: Text.Range, val info: Any)
   33.24 +  {
   33.25 +    def contains(that: Node): Boolean = this.range contains that.range
   33.26 +    def intersect(r: Text.Range): Node = Node(range.intersect(r), info)
   33.27 +  }
   33.28 +
   33.29 +
   33.30 +  /* branches sorted by quasi-order -- overlapping intervals appear as equivalent */
   33.31 +
   33.32 +  object Branches
   33.33 +  {
   33.34 +    type Entry = (Node, Markup_Tree)
   33.35 +    type T = SortedMap[Node, Entry]
   33.36 +
   33.37 +    val empty = SortedMap.empty[Node, Entry](new scala.math.Ordering[Node]
   33.38 +      {
   33.39 +        def compare(x: Node, y: Node): Int = x.range compare y.range
   33.40 +      })
   33.41 +    def update(branches: T, entries: Entry*): T =
   33.42 +      branches ++ entries.map(e => (e._1 -> e))
   33.43 +  }
   33.44 +
   33.45 +  val empty = new Markup_Tree(Branches.empty)
   33.46 +}
   33.47 +
   33.48 +
   33.49 +case class Markup_Tree(val branches: Markup_Tree.Branches.T)
   33.50 +{
   33.51 +  import Markup_Tree._
   33.52 +
   33.53 +  def + (new_node: Node): Markup_Tree =
   33.54 +  {
   33.55 +    branches.get(new_node) match {
   33.56 +      case None =>
   33.57 +        new Markup_Tree(Branches.update(branches, new_node -> empty))
   33.58 +      case Some((node, subtree)) =>
   33.59 +        if (node.range != new_node.range && node.contains(new_node))
   33.60 +          new Markup_Tree(Branches.update(branches, node -> (subtree + new_node)))
   33.61 +        else if (new_node.contains(branches.head._1) && new_node.contains(branches.last._1))
   33.62 +          new Markup_Tree(Branches.update(Branches.empty, (new_node -> this)))
   33.63 +        else {
   33.64 +          var overlapping = Branches.empty
   33.65 +          var rest = branches
   33.66 +          while (rest.isDefinedAt(new_node)) {
   33.67 +            overlapping = Branches.update(overlapping, rest(new_node))
   33.68 +            rest -= new_node
   33.69 +          }
   33.70 +          if (overlapping.forall(e => new_node.contains(e._1)))
   33.71 +            new Markup_Tree(Branches.update(rest, new_node -> new Markup_Tree(overlapping)))
   33.72 +          else { // FIXME split markup!?
   33.73 +            System.err.println("Ignored overlapping markup: " + new_node)
   33.74 +            this
   33.75 +          }
   33.76 +        }
   33.77 +    }
   33.78 +  }
   33.79 +
   33.80 +  // FIXME depth-first with result markup stack
   33.81 +  // FIXME projection to given range
   33.82 +  def flatten(parent: Node): List[Node] =
   33.83 +  {
   33.84 +    val result = new mutable.ListBuffer[Node]
   33.85 +    var offset = parent.range.start
   33.86 +    for ((_, (node, subtree)) <- branches.iterator) {
   33.87 +      if (offset < node.range.start)
   33.88 +        result += new Node(Text.Range(offset, node.range.start), parent.info)
   33.89 +      result ++= subtree.flatten(node)
   33.90 +      offset = node.range.stop
   33.91 +    }
   33.92 +    if (offset < parent.range.stop)
   33.93 +      result += new Node(Text.Range(offset, parent.range.stop), parent.info)
   33.94 +    result.toList
   33.95 +  }
   33.96 +
   33.97 +  def filter(pred: Node => Boolean): Markup_Tree =
   33.98 +  {
   33.99 +    val bs = branches.toList.flatMap(entry => {
  33.100 +      val (_, (node, subtree)) = entry
  33.101 +      if (pred(node)) List((node, (node, subtree.filter(pred))))
  33.102 +      else subtree.filter(pred).branches.toList
  33.103 +    })
  33.104 +    new Markup_Tree(Branches.empty ++ bs)
  33.105 +  }
  33.106 +
  33.107 +  def select[A](range: Text.Range)(sel: PartialFunction[Node, A]): Stream[Node] =
  33.108 +  {
  33.109 +    def stream(parent: Node, bs: Branches.T): Stream[Node] =
  33.110 +    {
  33.111 +      val start = Node(parent.range.start_range, Nil)
  33.112 +      val stop = Node(parent.range.stop_range, Nil)
  33.113 +      val substream =
  33.114 +        (for ((_, (node, subtree)) <- bs.range(start, stop).toStream) yield {
  33.115 +          if (sel.isDefinedAt(node))
  33.116 +            stream(node.intersect(parent.range), subtree.branches)
  33.117 +          else stream(parent, subtree.branches)
  33.118 +        }).flatten
  33.119 +
  33.120 +      def padding(last: Text.Offset, s: Stream[Node]): Stream[Node] =
  33.121 +        s match {
  33.122 +          case node #:: rest =>
  33.123 +            if (last < node.range.start)
  33.124 +              parent.intersect(Text.Range(last, node.range.start)) #::
  33.125 +                node #:: padding(node.range.stop, rest)
  33.126 +            else node #:: padding(node.range.stop, rest)
  33.127 +          case Stream.Empty =>  // FIXME
  33.128 +            if (last < parent.range.stop)
  33.129 +            Stream(parent.intersect(Text.Range(last, parent.range.stop)))
  33.130 +            else Stream.Empty
  33.131 +        }
  33.132 +      padding(parent.range.start, substream)
  33.133 +    }
  33.134 +    // FIXME handle disjoint range!?
  33.135 +    stream(Node(range, Nil), branches)
  33.136 +  }
  33.137 +
  33.138 +  def swing_tree(parent: DefaultMutableTreeNode)(swing_node: Node => DefaultMutableTreeNode)
  33.139 +  {
  33.140 +    for ((_, (node, subtree)) <- branches) {
  33.141 +      val current = swing_node(node)
  33.142 +      subtree.swing_tree(current)(swing_node)
  33.143 +      parent.add(current)
  33.144 +    }
  33.145 +  }
  33.146 +}
  33.147 +
    34.1 --- a/src/Pure/PIDE/text.scala	Thu Aug 19 16:08:59 2010 +0200
    34.2 +++ b/src/Pure/PIDE/text.scala	Thu Aug 19 17:41:52 2010 +0200
    34.3 @@ -10,15 +10,42 @@
    34.4  
    34.5  object Text
    34.6  {
    34.7 -  /* offset and range */
    34.8 +  /* offset */
    34.9  
   34.10    type Offset = Int
   34.11  
   34.12 +
   34.13 +  /* range: interval with total quasi-ordering */
   34.14 +
   34.15 +  object Range
   34.16 +  {
   34.17 +    object Ordering extends scala.math.Ordering[Range]
   34.18 +    {
   34.19 +      override def compare(r1: Range, r2: Range): Int = r1 compare r2
   34.20 +    }
   34.21 +  }
   34.22 +
   34.23    sealed case class Range(val start: Offset, val stop: Offset)
   34.24    {
   34.25 -    def contains(i: Offset): Boolean = start <= i && i < stop
   34.26 +    require(start <= stop)
   34.27 +
   34.28      def map(f: Offset => Offset): Range = Range(f(start), f(stop))
   34.29      def +(i: Offset): Range = map(_ + i)
   34.30 +    def contains(i: Offset): Boolean = start <= i && i < stop
   34.31 +    def contains(that: Range): Boolean =
   34.32 +      this == that || this.contains(that.start) && that.stop <= this.stop
   34.33 +    def overlaps(that: Range): Boolean =
   34.34 +      this == that || this.contains(that.start) || that.contains(this.start)
   34.35 +    def compare(that: Range): Int =
   34.36 +      if (overlaps(that)) 0
   34.37 +      else if (this.start < that.start) -1
   34.38 +      else 1
   34.39 +
   34.40 +    def start_range: Range = Range(start, start)
   34.41 +    def stop_range: Range = Range(stop, stop)
   34.42 +
   34.43 +    def intersect(that: Range): Range =
   34.44 +      Range(this.start max that.start, this.stop min that.stop)
   34.45    }
   34.46  
   34.47  
    35.1 --- a/src/Pure/ROOT.ML	Thu Aug 19 16:08:59 2010 +0200
    35.2 +++ b/src/Pure/ROOT.ML	Thu Aug 19 17:41:52 2010 +0200
    35.3 @@ -179,9 +179,9 @@
    35.4  use "ML/ml_syntax.ML";
    35.5  use "ML/ml_env.ML";
    35.6  use "Isar/runtime.ML";
    35.7 -if ml_system = "polyml-5.3.0"
    35.8 -then use "ML/ml_compiler_polyml-5.3.ML"
    35.9 -else use "ML/ml_compiler.ML";
   35.10 +if member (op =) ["polyml-5.2", "polyml-5.2.1", "smlnj-110"] ml_system
   35.11 +then use "ML/ml_compiler.ML"
   35.12 +else use "ML/ml_compiler_polyml-5.3.ML";
   35.13  use "ML/ml_context.ML";
   35.14  
   35.15  (*theory sources*)
   35.16 @@ -257,7 +257,7 @@
   35.17  
   35.18  use "System/session.ML";
   35.19  use "System/isabelle_process.ML";
   35.20 -use "System/isar_document.ML";
   35.21 +use "PIDE/isar_document.ML";
   35.22  use "System/isar.ML";
   35.23  
   35.24  
    36.1 --- a/src/Pure/Syntax/lexicon.ML	Thu Aug 19 16:08:59 2010 +0200
    36.2 +++ b/src/Pure/Syntax/lexicon.ML	Thu Aug 19 17:41:52 2010 +0200
    36.3 @@ -181,9 +181,9 @@
    36.4    | FloatSy     => Markup.numeral
    36.5    | XNumSy      => Markup.numeral
    36.6    | StrSy       => Markup.inner_string
    36.7 -  | Space       => Markup.none
    36.8 +  | Space       => Markup.empty
    36.9    | Comment     => Markup.inner_comment
   36.10 -  | EOF         => Markup.none;
   36.11 +  | EOF         => Markup.empty;
   36.12  
   36.13  fun report_token ctxt (Token (kind, _, (pos, _))) =
   36.14    Context_Position.report ctxt (token_kind_markup kind) pos;
    37.1 --- a/src/Pure/System/isar_document.ML	Thu Aug 19 16:08:59 2010 +0200
    37.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.3 @@ -1,42 +0,0 @@
    37.4 -(*  Title:      Pure/System/isar_document.ML
    37.5 -    Author:     Makarius
    37.6 -
    37.7 -Protocol commands for interactive Isar documents.
    37.8 -*)
    37.9 -
   37.10 -structure Isar_Document: sig end =
   37.11 -struct
   37.12 -
   37.13 -val global_state = Synchronized.var "Isar_Document" Document.init_state;
   37.14 -val change_state = Synchronized.change global_state;
   37.15 -
   37.16 -val _ =
   37.17 -  Isabelle_Process.add_command "Isar_Document.define_command"
   37.18 -    (fn [id, text] => change_state (Document.define_command (Document.parse_id id) text));
   37.19 -
   37.20 -val _ =
   37.21 -  Isabelle_Process.add_command "Isar_Document.edit_version"
   37.22 -    (fn [old_id_string, new_id_string, edits_yxml] => change_state (fn state =>
   37.23 -      let
   37.24 -        val old_id = Document.parse_id old_id_string;
   37.25 -        val new_id = Document.parse_id new_id_string;
   37.26 -        val edits =
   37.27 -          XML_Data.dest_list
   37.28 -            (XML_Data.dest_pair
   37.29 -              XML_Data.dest_string
   37.30 -              (XML_Data.dest_option
   37.31 -                (XML_Data.dest_list
   37.32 -                  (XML_Data.dest_pair
   37.33 -                    (XML_Data.dest_option XML_Data.dest_int)
   37.34 -                    (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits_yxml);
   37.35 -
   37.36 -      val (updates, state') = Document.edit old_id new_id edits state;
   37.37 -      val _ =
   37.38 -        implode (map (fn (id, exec_id) => Markup.markup (Markup.edit id exec_id) "") updates)
   37.39 -        |> Markup.markup (Markup.assign new_id)
   37.40 -        |> Output.status;
   37.41 -      val state'' = Document.execute new_id state';
   37.42 -    in state'' end));
   37.43 -
   37.44 -end;
   37.45 -
    38.1 --- a/src/Pure/System/isar_document.scala	Thu Aug 19 16:08:59 2010 +0200
    38.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.3 @@ -1,65 +0,0 @@
    38.4 -/*  Title:      Pure/System/isar_document.scala
    38.5 -    Author:     Makarius
    38.6 -
    38.7 -Protocol commands for interactive Isar documents.
    38.8 -*/
    38.9 -
   38.10 -package isabelle
   38.11 -
   38.12 -
   38.13 -object Isar_Document
   38.14 -{
   38.15 -  /* protocol messages */
   38.16 -
   38.17 -  object Assign {
   38.18 -    def unapply(msg: XML.Tree)
   38.19 -        : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
   38.20 -      msg match {
   38.21 -        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
   38.22 -          val id_edits = edits.map(Edit.unapply)
   38.23 -          if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
   38.24 -          else None
   38.25 -        case _ => None
   38.26 -      }
   38.27 -  }
   38.28 -
   38.29 -  object Edit {
   38.30 -    def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
   38.31 -      msg match {
   38.32 -        case XML.Elem(
   38.33 -          Markup(Markup.EDIT,
   38.34 -            List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
   38.35 -        case _ => None
   38.36 -      }
   38.37 -  }
   38.38 -}
   38.39 -
   38.40 -
   38.41 -trait Isar_Document extends Isabelle_Process
   38.42 -{
   38.43 -  import Isar_Document._
   38.44 -
   38.45 -
   38.46 -  /* commands */
   38.47 -
   38.48 -  def define_command(id: Document.Command_ID, text: String): Unit =
   38.49 -    input("Isar_Document.define_command", Document.ID(id), text)
   38.50 -
   38.51 -
   38.52 -  /* document versions */
   38.53 -
   38.54 -  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
   38.55 -      edits: List[Document.Edit[Document.Command_ID]])
   38.56 -  {
   38.57 -    val arg =
   38.58 -      XML_Data.make_list(
   38.59 -        XML_Data.make_pair(XML_Data.make_string)(
   38.60 -          XML_Data.make_option(XML_Data.make_list(
   38.61 -              XML_Data.make_pair(
   38.62 -                XML_Data.make_option(XML_Data.make_long))(
   38.63 -                XML_Data.make_option(XML_Data.make_long))))))(edits)
   38.64 -
   38.65 -    input("Isar_Document.edit_version",
   38.66 -      Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
   38.67 -  }
   38.68 -}
    39.1 --- a/src/Pure/Thy/thy_syntax.ML	Thu Aug 19 16:08:59 2010 +0200
    39.2 +++ b/src/Pure/Thy/thy_syntax.ML	Thu Aug 19 17:41:52 2010 +0200
    39.3 @@ -59,9 +59,9 @@
    39.4    | Token.String        => Markup.string
    39.5    | Token.AltString     => Markup.altstring
    39.6    | Token.Verbatim      => Markup.verbatim
    39.7 -  | Token.Space         => Markup.none
    39.8 +  | Token.Space         => Markup.empty
    39.9    | Token.Comment       => Markup.comment
   39.10 -  | Token.InternalValue => Markup.none
   39.11 +  | Token.InternalValue => Markup.empty
   39.12    | Token.Malformed     => Markup.malformed
   39.13    | Token.Error _       => Markup.malformed
   39.14    | Token.Sync          => Markup.control
   39.15 @@ -73,10 +73,8 @@
   39.16      let
   39.17        val kind = Token.kind_of tok;
   39.18        val props =
   39.19 -        if kind = Token.Command then
   39.20 -          (case Keyword.command_keyword (Token.content_of tok) of
   39.21 -            SOME k => Markup.properties [(Markup.kindN, Keyword.kind_of k)]
   39.22 -          | NONE => I)
   39.23 +        if kind = Token.Command
   39.24 +        then Markup.properties [(Markup.nameN, Token.content_of tok)]
   39.25          else I;
   39.26      in props (token_kind_markup kind) end;
   39.27  
    40.1 --- a/src/Pure/build-jars	Thu Aug 19 16:08:59 2010 +0200
    40.2 +++ b/src/Pure/build-jars	Thu Aug 19 17:41:52 2010 +0200
    40.3 @@ -29,6 +29,7 @@
    40.4    General/position.scala
    40.5    General/pretty.scala
    40.6    General/scan.scala
    40.7 +  General/sha1.scala
    40.8    General/symbol.scala
    40.9    General/xml.scala
   40.10    General/xml_data.scala
   40.11 @@ -40,7 +41,8 @@
   40.12    Isar/token.scala
   40.13    PIDE/command.scala
   40.14    PIDE/document.scala
   40.15 -  PIDE/markup_node.scala
   40.16 +  PIDE/isar_document.scala
   40.17 +  PIDE/markup_tree.scala
   40.18    PIDE/text.scala
   40.19    System/cygwin.scala
   40.20    System/download.scala
   40.21 @@ -49,7 +51,6 @@
   40.22    System/isabelle_process.scala
   40.23    System/isabelle_syntax.scala
   40.24    System/isabelle_system.scala
   40.25 -  System/isar_document.scala
   40.26    System/platform.scala
   40.27    System/session.scala
   40.28    System/session_manager.scala
    41.1 --- a/src/Pure/context_position.ML	Thu Aug 19 16:08:59 2010 +0200
    41.2 +++ b/src/Pure/context_position.ML	Thu Aug 19 17:41:52 2010 +0200
    41.3 @@ -9,6 +9,7 @@
    41.4    val is_visible: Proof.context -> bool
    41.5    val set_visible: bool -> Proof.context -> Proof.context
    41.6    val restore_visible: Proof.context -> Proof.context -> Proof.context
    41.7 +  val report_text: Proof.context -> Markup.T -> Position.T -> string -> unit
    41.8    val report: Proof.context -> Markup.T -> Position.T -> unit
    41.9  end;
   41.10  
   41.11 @@ -25,7 +26,9 @@
   41.12  val set_visible = Data.put;
   41.13  val restore_visible = set_visible o is_visible;
   41.14  
   41.15 -fun report ctxt markup pos =
   41.16 -  if is_visible ctxt then Position.report markup pos else ();
   41.17 +fun report_text ctxt markup pos txt =
   41.18 +  if is_visible ctxt then Position.report_text markup pos txt else ();
   41.19 +
   41.20 +fun report ctxt markup pos = report_text ctxt markup pos "";
   41.21  
   41.22  end;
    42.1 --- a/src/Pure/pure_setup.ML	Thu Aug 19 16:08:59 2010 +0200
    42.2 +++ b/src/Pure/pure_setup.ML	Thu Aug 19 17:41:52 2010 +0200
    42.3 @@ -18,8 +18,9 @@
    42.4  
    42.5  (* ML toplevel pretty printing *)
    42.6  
    42.7 -if String.isPrefix "smlnj" ml_system then ()
    42.8 -else toplevel_pp ["String", "string"] "ML_Syntax.pretty_string";
    42.9 +if String.isPrefix "polyml" ml_system
   42.10 +then toplevel_pp ["String", "string"] "ML_Syntax.pretty_string"
   42.11 +else ();
   42.12  
   42.13  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
   42.14  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
   42.15 @@ -39,15 +40,10 @@
   42.16  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
   42.17  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
   42.18  
   42.19 -if ml_system = "polyml-5.3.0"
   42.20 -then use "ML/install_pp_polyml-5.3.ML"
   42.21 -else if String.isPrefix "polyml" ml_system
   42.22 +if ml_system = "polyml-5.2" orelse ml_system = "polyml-5.2.1"
   42.23  then use "ML/install_pp_polyml.ML"
   42.24 -else ();
   42.25 -
   42.26 -if ml_system = "polyml-5.0" orelse ml_system = "polyml-5.1" then
   42.27 -  Secure.use_text ML_Parse.global_context (0, "") false
   42.28 -    "PolyML.Compiler.maxInlineSize := 20"
   42.29 +else if String.isPrefix "polyml" ml_system
   42.30 +then use "ML/install_pp_polyml-5.3.ML"
   42.31  else ();
   42.32  
   42.33  
    43.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 19 16:08:59 2010 +0200
    43.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 19 17:41:52 2010 +0200
    43.3 @@ -279,7 +279,7 @@
    43.4        for {
    43.5          (command, command_start) <-
    43.6            snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
    43.7 -        markup <- snapshot.state(command).highlight.flatten
    43.8 +        markup <- snapshot.state(command).highlight
    43.9          val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
   43.10          if (abs_stop > start)
   43.11          if (abs_start < stop)
    44.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 19 16:08:59 2010 +0200
    44.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 19 17:41:52 2010 +0200
    44.3 @@ -79,7 +79,7 @@
    44.4        case Some((word, cs)) =>
    44.5          val ds =
    44.6            (if (Isabelle_Encoding.is_active(buffer))
    44.7 -            cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
    44.8 +            cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
    44.9             else cs).filter(_ != word)
   44.10          if (ds.isEmpty) null
   44.11          else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
   44.12 @@ -129,7 +129,7 @@
   44.13      val root = data.root
   44.14      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   44.15      for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
   44.16 -      root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
   44.17 +      snapshot.state(command).markup_root.swing_tree(root)((node: Markup_Tree.Node) =>
   44.18            {
   44.19              val content = command.source(node.range).replace('\n', ' ')
   44.20              val id = command.id
   44.21 @@ -146,7 +146,7 @@
   44.22                override def getEnd: Position = command_start + node.range.stop
   44.23                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
   44.24              })
   44.25 -          }))
   44.26 +          })
   44.27      }
   44.28    }
   44.29  }