refer to thy_load command of auxiliary file;
authorwenzelm
Wed Nov 20 12:24:54 2013 +0100 (2013-11-20)
changeset 54528842adea880a4
parent 54527 bfeb0ea6c2c0
child 54529 2ea4d717d152
refer to thy_load command of auxiliary file;
src/Pure/PIDE/document.scala
src/Tools/jEdit/src/jedit_editor.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Nov 20 12:04:06 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Nov 20 12:24:54 2013 +0100
     1.3 @@ -253,6 +253,14 @@
     1.4      def entries: Iterator[(Node.Name, Node)] =
     1.5        graph.entries.map({ case (name, (node, _)) => (name, node) })
     1.6  
     1.7 +    def thy_load_commands(file_name: Node.Name): List[Command] =
     1.8 +      (for {
     1.9 +        (_, node) <- entries
    1.10 +        cmd <- node.thy_load_commands.iterator
    1.11 +        Exn.Res((name, _)) <- cmd.blobs.iterator
    1.12 +        if name == file_name
    1.13 +      } yield cmd).toList
    1.14 +
    1.15      def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
    1.16      def topological_order: List[Node.Name] = graph.topological_order
    1.17    }
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 12:04:06 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 12:24:54 2013 +0100
     2.3 @@ -63,11 +63,13 @@
     2.4      Swing_Thread.require()
     2.5  
     2.6      val text_area = view.getTextArea
     2.7 +    val buffer = view.getBuffer
     2.8 +
     2.9      PIDE.document_view(text_area) match {
    2.10        case Some(doc_view) =>
    2.11          val node = snapshot.version.nodes(doc_view.model.node_name)
    2.12          val caret = snapshot.revert(text_area.getCaretPosition)
    2.13 -        if (caret < text_area.getBuffer.getLength) {
    2.14 +        if (caret < buffer.getLength) {
    2.15            val caret_commands = node.command_range(caret)
    2.16            if (caret_commands.hasNext) {
    2.17              val (cmd0, _) = caret_commands.next
    2.18 @@ -76,7 +78,15 @@
    2.19            else None
    2.20          }
    2.21          else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
    2.22 -      case None => None
    2.23 +      case None =>
    2.24 +        PIDE.document_model(buffer) match {
    2.25 +          case Some(model) if !model.node_name.is_theory =>
    2.26 +            snapshot.version.nodes.thy_load_commands(model.node_name) match {
    2.27 +              case cmd :: _ => Some(cmd)
    2.28 +              case Nil => None
    2.29 +            }
    2.30 +          case _ => None
    2.31 +        }
    2.32      }
    2.33    }
    2.34