# HG changeset patch # User Lars Hupel # Date 1535228052 -7200 # Node ID 51fdede038c9fc99ff76f671efec386173dec563 # Parent db97c1ed115e0f8a249e151d0541878239761f4b# Parent f6c88cb715db09ce3e14f804cc1dd4905538e4bd merged diff -r db97c1ed115e -r 51fdede038c9 NEWS --- 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) --------------------------------- diff -r db97c1ed115e -r 51fdede038c9 src/Doc/Isar_Ref/Document_Preparation.thy --- 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} & : & \antiquotation\ \\ @{antiquotation_def type} & : & \antiquotation\ \\ @{antiquotation_def class} & : & \antiquotation\ \\ + @{antiquotation_def locale} & : & \antiquotation\ \\ @{antiquotation_def "text"} & : & \antiquotation\ \\ @{antiquotation_def goals} & : & \antiquotation\ \\ @{antiquotation_def subgoals} & : & \antiquotation\ \\ @@ -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> \@{class c}\ prints a class \c\. + \<^descr> \@{locale c}\ prints a locale \c\. + \<^descr> \@{command name}\, \@{method name}\, \@{attribute name}\ print checked entities of the Isar language. diff -r db97c1ed115e -r 51fdede038c9 src/Doc/System/Sessions.thy --- 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}+) \} \<^descr> \isakeyword{session}~\A = B + body\ defines a new session \A\ based on diff -r db97c1ed115e -r 51fdede038c9 src/Pure/Concurrent/counter.ML --- 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; diff -r db97c1ed115e -r 51fdede038c9 src/Pure/General/exn.scala --- 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") } diff -r db97c1ed115e -r 51fdede038c9 src/Pure/ML_Bootstrap.thy --- 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 \ 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; \ \ diff -r db97c1ed115e -r 51fdede038c9 src/Pure/PIDE/prover.scala --- 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*) diff -r db97c1ed115e -r 51fdede038c9 src/Pure/PIDE/session.scala --- 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() diff -r db97c1ed115e -r 51fdede038c9 src/Pure/System/command_line.scala --- 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) diff -r db97c1ed115e -r 51fdede038c9 src/Pure/Thy/document_antiquotations.ML --- 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>\const\ (Args.const {proper = true, strict = false}) pretty_const #> basic_entity \<^binding>\abbrev\ (Scan.lift Args.embedded_inner_syntax) pretty_abbrev #> basic_entity \<^binding>\typ\ Args.typ_abbrev Syntax.pretty_typ #> - basic_entity \<^binding>\locale\ (Scan.lift (Parse.position Args.name)) pretty_locale #> + basic_entity \<^binding>\locale\ (Scan.lift (Parse.position Args.embedded)) pretty_locale #> basic_entity \<^binding>\class\ (Scan.lift Args.embedded_inner_syntax) pretty_class #> basic_entity \<^binding>\type\ (Scan.lift Args.embedded) pretty_type #> basic_entity \<^binding>\theory\ (Scan.lift (Parse.position Args.embedded)) pretty_theory #> diff -r db97c1ed115e -r 51fdede038c9 src/Pure/Thy/sessions.ML --- 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 diff -r db97c1ed115e -r 51fdede038c9 src/Pure/Thy/sessions.scala --- 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) ~!