--- a/NEWS Sat Aug 25 20:44:09 2018 +0200
+++ b/NEWS Sat Aug 25 22:14:12 2018 +0200
@@ -23,6 +23,13 @@
retained as migration auxiliary. INCOMPATIBILITY.
+*** ML ***
+
+* Original PolyML.pointerEq is retained as a convenience for tools that
+don't use Isabelle/ML (where this is called "pointer_eq").
+
+
+
New in Isabelle2018 (August 2018)
---------------------------------
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sat Aug 25 22:14:12 2018 +0200
@@ -94,6 +94,7 @@
@{antiquotation_def typ} & : & \<open>antiquotation\<close> \\
@{antiquotation_def type} & : & \<open>antiquotation\<close> \\
@{antiquotation_def class} & : & \<open>antiquotation\<close> \\
+ @{antiquotation_def locale} & : & \<open>antiquotation\<close> \\
@{antiquotation_def "text"} & : & \<open>antiquotation\<close> \\
@{antiquotation_def goals} & : & \<open>antiquotation\<close> \\
@{antiquotation_def subgoals} & : & \<open>antiquotation\<close> \\
@@ -180,6 +181,7 @@
@@{antiquotation typ} options @{syntax type} |
@@{antiquotation type} options @{syntax embedded} |
@@{antiquotation class} options @{syntax embedded} |
+ @@{antiquotation locale} options @{syntax embedded} |
(@@{antiquotation command} | @@{antiquotation method} | @@{antiquotation attribute})
options @{syntax name}
;
@@ -252,6 +254,8 @@
\<^descr> \<open>@{class c}\<close> prints a class \<open>c\<close>.
+ \<^descr> \<open>@{locale c}\<close> prints a locale \<open>c\<close>.
+
\<^descr> \<open>@{command name}\<close>, \<open>@{method name}\<close>, \<open>@{attribute name}\<close> print checked
entities of the Isar language.
--- a/src/Doc/System/Sessions.thy Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Doc/System/Sessions.thy Sat Aug 25 22:14:12 2018 +0200
@@ -58,7 +58,7 @@
;
groups: '(' (@{syntax name} +) ')'
;
- dir: @'in' @{syntax name}
+ dir: @'in' @{syntax embedded}
;
description: @'description' @{syntax text}
;
@@ -74,9 +74,9 @@
;
theory_entry: @{syntax system_name} ('(' @'global' ')')?
;
- document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
+ document_files: @'document_files' ('(' dir ')')? (@{syntax embedded}+)
;
- export_files: @'export_files' ('(' dir ')')? (@{syntax name}+)
+ export_files: @'export_files' ('(' dir ')')? (@{syntax embedded}+)
\<close>}
\<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
--- a/src/Pure/Concurrent/counter.ML Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/Concurrent/counter.ML Sat Aug 25 22:14:12 2018 +0200
@@ -20,8 +20,10 @@
fun next () =
Synchronized.change_result counter
(fn i =>
- let val j = i + (if Thread_Data.is_virtual then 3 else 2)
- in (j, j) end);
+ let
+ val k = i + 1;
+ val n = if Thread_Data.is_virtual then 2 * k + 1 else 2 * k;
+ in (n, k) end);
in next end;
end;
--- a/src/Pure/General/exn.scala Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/General/exn.scala Sat Aug 25 22:14:12 2018 +0200
@@ -138,4 +138,10 @@
def message(exn: Throwable): String =
user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
+
+
+ /* trace */
+
+ def trace(exn: Throwable): String =
+ exn.getStackTrace.mkString("\n")
}
--- a/src/Pure/ML_Bootstrap.thy Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/ML_Bootstrap.thy Sat Aug 25 22:14:12 2018 +0200
@@ -30,7 +30,11 @@
Context.setmp_generic_context NONE
ML \<open>
List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
- structure PolyML = struct structure IntInf = PolyML.IntInf end;
+ structure PolyML =
+ struct
+ val pointerEq = pointer_eq;
+ structure IntInf = PolyML.IntInf;
+ end;
\<close>
\<close>
--- a/src/Pure/PIDE/prover.scala Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/PIDE/prover.scala Sat Aug 25 22:14:12 2018 +0200
@@ -345,8 +345,8 @@
def protocol_command_bytes(name: String, args: Bytes*): Unit =
command_input match {
- case Some(thread) => thread.send(Bytes(name) :: args.toList)
- case None => error("Uninitialized command input thread")
+ case Some(thread) if thread.is_active => thread.send(Bytes(name) :: args.toList)
+ case _ => error("Inactive prover input thread for command " + quote(name))
}
def protocol_command(name: String, args: String*)
--- a/src/Pure/PIDE/session.scala Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/PIDE/session.scala Sat Aug 25 22:14:12 2018 +0200
@@ -307,18 +307,25 @@
private val delay =
Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
- private val changed_nodes = Synchronized(Set.empty[Document.Node.Name])
+ private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
+ private val state = Synchronized(init_state)
+
+ def exit()
+ {
+ delay.revoke()
+ state.change(_ => None)
+ }
def update(new_nodes: Set[Document.Node.Name] = Set.empty)
{
- changed_nodes.change(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)
- delay.invoke()
+ val active =
+ state.change_result(st =>
+ (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
+ if (active) delay.invoke()
}
def flush(): Set[Document.Node.Name] =
- changed_nodes.change_result(nodes => (nodes, Set.empty))
-
- def revoke() { delay.revoke() }
+ state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None))
}
@@ -549,7 +556,7 @@
prover.set(start_prover(manager.send(_)))
case Stop =>
- consolidation.revoke()
+ consolidation.exit()
delay_prune.revoke()
if (prover.defined) {
protocol_handlers.exit()
--- a/src/Pure/System/command_line.scala Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/System/command_line.scala Sat Aug 25 22:14:12 2018 +0200
@@ -29,8 +29,7 @@
try { body }
catch {
case exn: Throwable =>
- if (debug) exn.printStackTrace
- Output.error_message(Exn.message(exn))
+ Output.error_message(Exn.message(exn) + (if (debug) "\n" + Exn.trace(exn) else ""))
Exn.return_code(exn, 2)
}
sys.exit(rc)
--- a/src/Pure/Thy/document_antiquotations.ML Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Sat Aug 25 22:14:12 2018 +0200
@@ -80,7 +80,7 @@
basic_entity \<^binding>\<open>const\<close> (Args.const {proper = true, strict = false}) pretty_const #>
basic_entity \<^binding>\<open>abbrev\<close> (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #>
basic_entity \<^binding>\<open>typ\<close> Args.typ_abbrev Syntax.pretty_typ #>
- basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.name)) pretty_locale #>
+ basic_entity \<^binding>\<open>locale\<close> (Scan.lift (Parse.position Args.embedded)) pretty_locale #>
basic_entity \<^binding>\<open>class\<close> (Scan.lift Args.embedded_inner_syntax) pretty_class #>
basic_entity \<^binding>\<open>type\<close> (Scan.lift Args.embedded) pretty_type #>
basic_entity \<^binding>\<open>theory\<close> (Scan.lift (Parse.position Args.embedded)) pretty_theory #>
--- a/src/Pure/Thy/sessions.ML Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/Thy/sessions.ML Sat Aug 25 22:14:12 2018 +0200
@@ -37,7 +37,7 @@
val export_files =
Parse.$$$ "export_files" |--
- Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.name);
+ Parse.!!! (Scan.optional in_path ("export", Position.none) -- Scan.repeat1 Parse.embedded);
in
--- a/src/Pure/Thy/sessions.scala Sat Aug 25 20:44:09 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Sat Aug 25 22:14:12 2018 +0200
@@ -815,7 +815,7 @@
((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
val export_files =
- $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(name)) ^^
+ $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ rep1(embedded)) ^^
{ case _ ~ (x ~ y) => (x, y) }
command(SESSION) ~!