# HG changeset patch
# User wenzelm
# Date 1671446565 -3600
# Node ID 94cdf6513f01b471e3c6410f237326eb848f7f56
# Parent  3543ecb4c97d266d3829e60e128cef821324068f
clarified signature;

diff -r 3543ecb4c97d -r 94cdf6513f01 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Dec 19 11:16:46 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Mon Dec 19 11:42:45 2022 +0100
@@ -85,12 +85,13 @@
 
 val no_header: node_header =
   {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
-val no_perspective = make_perspective (false, [], []);
+
+val empty_perspective = make_perspective (false, [], []);
 
 val empty_node =
-  make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
+  make_node (no_header, NONE, empty_perspective, Entries.empty, NONE, Lazy.value ());
 
-fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
+fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
   Inttab.is_empty visible andalso
   is_none visible_last andalso
@@ -99,7 +100,7 @@
 fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
   header = no_header andalso
   is_none keywords andalso
-  is_no_perspective perspective andalso
+  is_empty_perspective perspective andalso
   Entries.is_empty entries andalso
   is_none result andalso
   Lazy.is_finished consolidated;
diff -r 3543ecb4c97d -r 94cdf6513f01 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Dec 19 11:16:46 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Dec 19 11:42:45 2022 +0100
@@ -181,24 +181,23 @@
 
     /* perspective */
 
-    type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
-    type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
-
-    val no_perspective_text: Perspective_Text =
-      Perspective(false, Text.Perspective.empty, Overlays.empty)
-
-    val no_perspective_command: Perspective_Command =
-      Perspective(false, Command.Perspective.empty, Overlays.empty)
+    object Perspective_Text {
+      type T = Perspective[Text.Edit, Text.Perspective]
+      val empty: T = Perspective(false, Text.Perspective.empty, Overlays.empty)
+      def is_empty(perspective: T): Boolean =
+        !perspective.required &&
+        perspective.visible.is_empty &&
+        perspective.overlays.is_empty
+    }
 
-    def is_no_perspective_text(perspective: Perspective_Text): Boolean =
-      !perspective.required &&
-      perspective.visible.is_empty &&
-      perspective.overlays.is_empty
-
-    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
-      !perspective.required &&
-      perspective.visible.is_empty &&
-      perspective.overlays.is_empty
+    object Perspective_Command {
+      type T = Perspective[Command.Edit, Command.Perspective]
+      val empty: T = Perspective(false, Command.Perspective.empty, Overlays.empty)
+      def is_empty(perspective: T): Boolean =
+        !perspective.required &&
+        perspective.visible.is_empty &&
+        perspective.overlays.is_empty
+    }
 
 
     /* commands */
@@ -272,14 +271,14 @@
     val header: Node.Header = Node.no_header,
     val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
-    val perspective: Node.Perspective_Command = Node.no_perspective_command,
+    val perspective: Node.Perspective_Command.T = Node.Perspective_Command.empty,
     _commands: Node.Commands = Node.Commands.empty
   ) {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
       text_perspective.is_empty &&
-      Node.is_no_perspective_command(perspective) &&
+      Node.Perspective_Command.is_empty(perspective) &&
       commands.isEmpty
 
     def has_header: Boolean = header != Node.no_header
@@ -304,7 +303,7 @@
 
     def update_perspective(
         new_text_perspective: Text.Perspective,
-        new_perspective: Node.Perspective_Command): Node =
+        new_perspective: Node.Perspective_Command.T): Node =
       new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
 
     def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
@@ -312,7 +311,7 @@
 
     def same_perspective(
         other_text_perspective: Text.Perspective,
-        other_perspective: Node.Perspective_Command): Boolean =
+        other_perspective: Node.Perspective_Command.T): Boolean =
       text_perspective == other_text_perspective &&
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
@@ -770,7 +769,7 @@
     def node_edits(
       node_header: Node.Header,
       text_edits: List[Text.Edit],
-      perspective: Node.Perspective_Text
+      perspective: Node.Perspective_Text.T
     ): List[Edit_Text] = {
       val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
         get_blob match {
diff -r 3543ecb4c97d -r 94cdf6513f01 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Dec 19 11:16:46 2022 +0100
+++ b/src/Pure/PIDE/headless.scala	Mon Dec 19 11:42:45 2022 +0100
@@ -471,7 +471,7 @@
     ) {
       override def toString: String = node_name.toString
 
-      def node_perspective: Document.Node.Perspective_Text =
+      def node_perspective: Document.Node.Perspective_Text.T =
         Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
 
       def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
diff -r 3543ecb4c97d -r 94cdf6513f01 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Dec 19 11:16:46 2022 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Dec 19 11:42:45 2022 +0100
@@ -258,7 +258,7 @@
 
       case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
-        val perspective: Document.Node.Perspective_Command =
+        val perspective: Document.Node.Perspective_Command.T =
           Document.Node.Perspective(required, visible_overlay, overlays)
         if (node.same_perspective(text_perspective, perspective)) node
         else {
diff -r 3543ecb4c97d -r 94cdf6513f01 src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 19 11:16:46 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 19 11:42:45 2022 +0100
@@ -72,7 +72,7 @@
   external_file: Boolean = false,
   theory_required: Boolean = false,
   document_required: Boolean = false,
-  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+  last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
   pending_edits: List[Text.Edit] = Nil,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil,
   published_decorations: List[VSCode_Model.Decoration] = Nil
@@ -111,7 +111,7 @@
   def node_perspective(
     doc_blobs: Document.Blobs,
     caret: Option[Line.Position]
-  ): (Boolean, Document.Node.Perspective_Text) = {
+  ): (Boolean, Document.Node.Perspective_Text.T) = {
     if (is_theory) {
       val snapshot = model.snapshot()
 
@@ -144,7 +144,7 @@
       (snapshot.node.load_commands_changed(doc_blobs),
         Document.Node.Perspective(node_required, text_perspective, overlays))
     }
-    else (false, Document.Node.no_perspective_text)
+    else (false, Document.Node.Perspective_Text.empty)
   }
 
 
diff -r 3543ecb4c97d -r 94cdf6513f01 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 19 11:16:46 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 19 11:42:45 2022 +0100
@@ -340,7 +340,7 @@
   def node_perspective(
     doc_blobs: Document.Blobs,
     hidden: Boolean
-  ): (Boolean, Document.Node.Perspective_Text) = {
+  ): (Boolean, Document.Node.Perspective_Text.T) = {
     GUI_Thread.require {}
 
     if (JEdit_Options.continuous_checking() && is_theory) {
@@ -358,7 +358,7 @@
 
       (reparse, Document.Node.Perspective(node_required, perspective, overlays))
     }
-    else (false, Document.Node.no_perspective_text)
+    else (false, Document.Node.Perspective_Text.empty)
   }
 
 
@@ -377,14 +377,14 @@
 object File_Model {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
-      false, false, Document.Node.no_perspective_text, Nil)
+      false, false, Document.Node.Perspective_Text.empty, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
     theory_required: Boolean = false,
     document_required: Boolean = false,
-    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+    last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
     val file = JEdit_Lib.check_file(node_name.node)
@@ -404,7 +404,7 @@
   content: Document_Model.File_Content,
   theory_required: Boolean,
   document_required: Boolean,
-  last_perspective: Document.Node.Perspective_Text,
+  last_perspective: Document.Node.Perspective_Text.T,
   pending_edits: List[Text.Edit]
 ) extends Document_Model {
   /* required */
@@ -469,10 +469,10 @@
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
         !File_Format.registry.is_theory(node_name) &&
-          (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
+          (node_required || !Document.Node.Perspective_Text.is_empty(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))
-      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
+      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty))
     }
 
 
@@ -586,12 +586,12 @@
 
   private object pending_edits {
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective = Document.Node.no_perspective_text
+    private var last_perspective = Document.Node.Perspective_Text.empty
 
     def nonEmpty: Boolean = synchronized { pending.nonEmpty }
     def get_edits: List[Text.Edit] = synchronized { pending.toList }
-    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
-    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
+    def get_last_perspective: Document.Node.Perspective_Text.T = synchronized { last_perspective }
+    def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
       synchronized { last_perspective = perspective }
 
     def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =