# HG changeset patch # User wenzelm # Date 1649108774 -7200 # Node ID 85e8b4c2b9a9e91533395f405b88cf985adb9428 # Parent b13ab7d11b902e8f0dcb7185fb5a35d0389807d9 clarified signature: avoid ambiguity in scala3; diff -r b13ab7d11b90 -r 85e8b4c2b9a9 src/Pure/General/json.scala --- 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) { diff -r b13ab7d11b90 -r 85e8b4c2b9a9 src/Pure/PIDE/headless.scala --- 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() diff -r b13ab7d11b90 -r 85e8b4c2b9a9 src/Pure/PIDE/resources.scala --- 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 diff -r b13ab7d11b90 -r 85e8b4c2b9a9 src/Pure/Thy/sessions.scala --- 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"