src/Pure/Thy/sessions.scala
changeset 65254 3075aa3b40bf
parent 65251 4b0a43afc3fb
child 65269 2947837b9f04
equal deleted inserted replaced
65253:85c0ac5c2589 65254:3075aa3b40bf
    25     val roots = Thy_Header.ml_roots.map(_._1)
    25     val roots = Thy_Header.ml_roots.map(_._1)
    26     val loaded_files =
    26     val loaded_files =
    27       roots.flatMap(root => resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
    27       roots.flatMap(root => resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
    28     (roots ::: loaded_files).map(file => dir + Path.explode(file))
    28     (roots ::: loaded_files).map(file => dir + Path.explode(file))
    29   }
    29   }
       
    30 
       
    31   def pure_base(options: Options): Base = session_base(options, Thy_Header.PURE)
    30 
    32 
    31 
    33 
    32   /* base info and source dependencies */
    34   /* base info and source dependencies */
    33 
    35 
    34   object Base
    36   object Base