src/Tools/jEdit/src/rendering.scala
changeset 50205 788c8263e634
parent 50202 ec0f2f8dbeb9
child 50206 6626bc5ed053
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:31:49 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:59:32 2012 +0100
     1.3 @@ -205,7 +205,7 @@
     1.4          {
     1.5            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
     1.6            if Path.is_ok(name) =>
     1.7 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
     1.8 +            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
     1.9              Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
    1.10  
    1.11            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    1.12 @@ -304,7 +304,7 @@
    1.13              add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
    1.14            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
    1.15            if Path.is_ok(name) =>
    1.16 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    1.17 +            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    1.18              add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
    1.19            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    1.20            if name == Markup.SORTING || name == Markup.TYPING =>