clarified signature: avoid ambiguity in scala3;
authorwenzelm
Mon, 04 Apr 2022 23:46:14 +0200
changeset 75406 85e8b4c2b9a9
parent 75405 b13ab7d11b90
child 75407 c7051638a38c
clarified signature: avoid ambiguity in scala3;
src/Pure/General/json.scala
src/Pure/PIDE/headless.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.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) {
--- 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"