updated thy_info.dependencies;
authorwenzelm
Fri, 14 Feb 2014 14:51:38 +0100
changeset 55490 9b0fb0e2c9f5
parent 55489 c12ad7295f57
child 55491 74db756853d4
updated thy_info.dependencies;
src/Pure/General/position.scala
src/Tools/jEdit/src/plugin.scala
--- a/src/Pure/General/position.scala	Fri Feb 14 14:44:43 2014 +0100
+++ b/src/Pure/General/position.scala	Fri Feb 14 14:51:38 2014 +0100
@@ -14,6 +14,8 @@
 {
   type T = Properties.T
 
+  val none: T = Nil
+
   val Line = new Properties.Int(Markup.LINE)
   val Offset = new Properties.Int(Markup.OFFSET)
   val End_Offset = new Properties.Int(Markup.END_OFFSET)
--- a/src/Tools/jEdit/src/plugin.scala	Fri Feb 14 14:44:43 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Feb 14 14:51:38 2014 +0100
@@ -173,7 +173,7 @@
               buffer <- buffers
               model <- PIDE.document_model(buffer)
               if model.is_theory
-            } yield model.node_name
+            } yield (model.node_name, Position.none)
 
           val thy_info = new Thy_Info(PIDE.thy_load)
           // FIXME avoid I/O in Swing thread!?!