# HG changeset patch
# User wenzelm
# Date 1392385898 -3600
# Node ID 9b0fb0e2c9f579b60053dba2cf185a2acc55875e
# Parent  c12ad7295f57a0e09d9a00c7777d0d6ed16cacbc
updated thy_info.dependencies;

diff -r c12ad7295f57 -r 9b0fb0e2c9f5 src/Pure/General/position.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)
diff -r c12ad7295f57 -r 9b0fb0e2c9f5 src/Tools/jEdit/src/plugin.scala
--- 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!?!