# HG changeset patch # User wenzelm # Date 1674037947 -3600 # Node ID 8ecf99ac5359eab4b94cc91b0f4e0a8dfa4b855c # Parent ffc0774e0efe86d419813aab7c72ca675a337915 tuned; diff -r ffc0774e0efe -r 8ecf99ac5359 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jan 17 16:56:27 2023 +0100 +++ b/src/Pure/PIDE/document.scala Wed Jan 18 11:32:27 2023 +0100 @@ -674,8 +674,10 @@ if (command_node.commands.contains(command)) Some((command_node, command)) else None } - def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) - : Option[Line.Node_Position] = + def find_command_position( + id: Document_ID.Generic, + offset: Symbol.Offset + ): Option[Line.Node_Position] = { for ((node, command) <- find_command(id)) yield { val name = command.node_name.node @@ -686,6 +688,7 @@ val pos = sources_iterator.foldLeft(Line.Position.zero)(_.advance(_)) Line.Node_Position(name, pos) } + } def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] = if (other_node_name.is_theory) {