# 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] =