--- 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
--- /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"
--- 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)
---------------------------------
--- 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.
--- 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
--- 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
--- 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"
--- 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"
--- 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"
--- 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;
--- 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"
--- 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) }
}
--- 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];
--- /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))
+}
+
--- 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(_))
}
--- 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);
--- 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 */
--- 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 =
--- 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)
}
}
--- 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 \
--- 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)
--- 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
}
}
--- 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;
--- 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
--- 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;
-
--- 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;
-
--- 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";
--- 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
--- 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)
}
--- /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;
+
--- /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))
+ }
+}
--- 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)
- }
-}
--- /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)
+ }
+ }
+}
+
--- 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)
}
--- 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";
--- 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;
--- 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;
-
--- 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))
- }
-}
--- 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;
--- 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
--- 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;
--- 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 ();
--- 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)
--- 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 + "]"
})
- }))
+ })
}
}
}