src/Tools/jEdit/src/rendering.scala

   {
     snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
             Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
           if !props.exists(
             { case (Markup.KIND, Markup.ML_OPEN) => true

           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
             val kind1 = space_explode('_', kind).mkString(" ")
             add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
             add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
             add(prev, r, (true, pretty_typing("::", body)))
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>