src/Pure/PIDE/resources.scala
changeset 64839 842163abfc0d
parent 64835 fd1efd6dd385
child 64854 f5aa712e6250
     1.1 --- a/src/Pure/PIDE/resources.scala	Sun Jan 08 17:36:00 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sun Jan 08 17:42:31 2017 +0100
     1.3 @@ -26,6 +26,9 @@
     1.4    val base_syntax: Outer_Syntax,
     1.5    val log: Logger = No_Logger)
     1.6  {
     1.7 +  val thy_info = new Thy_Info(this)
     1.8 +
     1.9 +
    1.10    /* document node names */
    1.11  
    1.12    def node_name(qualifier: String, raw_path: Path): Document.Node.Name =