--- a/src/Pure/General/json.scala Mon Apr 04 23:33:14 2022 +0200
+++ b/src/Pure/General/json.scala Mon Apr 04 23:46:14 2022 +0200
@@ -39,7 +39,7 @@
/* lexer */
object Kind extends Enumeration {
- val KEYWORD, STRING, NUMBER, ERROR = Value
+ val KEYWORD, STRING, NUMBER, ERROR = this.Value
}
sealed case class Token(kind: Kind.Value, text: String) {
--- a/src/Pure/PIDE/headless.scala Mon Apr 04 23:33:14 2022 +0200
+++ b/src/Pure/PIDE/headless.scala Mon Apr 04 23:46:14 2022 +0200
@@ -313,7 +313,7 @@
}
}
- Session.Consumer[Session.Commands_Changed](getClass.getName) {
+ isabelle.Session.Consumer[isabelle.Session.Commands_Changed](getClass.getName) {
case changed =>
if (changed.nodes.exists(dep_theories_set)) {
val snapshot = session.snapshot()
--- a/src/Pure/PIDE/resources.scala Mon Apr 04 23:33:14 2022 +0200
+++ b/src/Pure/PIDE/resources.scala Mon Apr 04 23:46:14 2022 +0200
@@ -246,7 +246,7 @@
def special_header(name: Document.Node.Name): Option[Document.Node.Header] = {
val imports =
- if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
+ if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_import))
else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
else Nil
--- a/src/Pure/Thy/sessions.scala Mon Apr 04 23:33:14 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Mon Apr 04 23:46:14 2022 +0200
@@ -23,7 +23,7 @@
val roots_name: String = "ROOTS"
val root_name: String = "ROOT"
- val theory_name: String = "Pure.Sessions"
+ val theory_import: String = "Pure.Sessions"
val UNSORTED = "Unsorted"
val DRAFT = "Draft"