src/Pure/PIDE/resources.scala

 import scala.util.parsing.input.Reader
 
 import java.io.{File => JFile}
 
 
-object Resources
-{
+object Resources {
   def empty: Resources =
     new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
 
   def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
     empty.file_node(file, dir = dir, theory = theory)

 
 class Resources(
   val sessions_structure: Sessions.Structure,
   val session_base: Sessions.Base,
   val log: Logger = No_Logger,
-  command_timings: List[Properties.T] = Nil)
-{
+  command_timings: List[Properties.T] = Nil
+) {
   resources =>
 
 
   /* init session */
 
-  def init_session_yxml: String =
-  {
+  def init_session_yxml: String = {
     import XML.Encode._
 
     YXML.string_of_body(
       pair(list(pair(string, properties)),
       pair(list(pair(string, string)),

     (Path.explode(dir) + source_path).expand.implode
 
   def append(node_name: Document.Node.Name, source_path: Path): String =
     append(node_name.master_dir, source_path)
 
-  def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
-  {
+  def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = {
     val node = append(dir, file)
     val master_dir = append(dir, file.dir)
     Document.Node.Name(node, master_dir, theory)
   }
 

     Document.Node.Name(theory, "", theory)
 
 
   /* source files of Isabelle/ML bootstrap */
 
-  def source_file(raw_name: String): Option[String] =
-  {
+  def source_file(raw_name: String): Option[String] = {
     if (Path.is_wellformed(raw_name)) {
       if (Path.is_valid(raw_name)) {
         def check(p: Path): Option[Path] = if (p.is_file) Some(p) else None
 
         val path = Path.explode(raw_name)

   }
 
 
   /* theory files */
 
-  def load_commands(syntax: Outer_Syntax, name: Document.Node.Name)
-    : () => List[Command_Span.Span] =
-  {
+  def load_commands(
+    syntax: Outer_Syntax,
+    name: Document.Node.Name
+  ) : () => List[Command_Span.Span] = {
     val (is_utf8, raw_text) =
       with_thy_reader(name, reader => (Scan.reader_is_utf8(reader), reader.source.toString))
     () =>
       {
         if (syntax.has_load_commands(raw_text)) {

         }
         else Nil
       }
   }
 
-  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name, spans: List[Command_Span.Span])
-    : List[Path] =
-  {
+  def loaded_files(
+    syntax: Outer_Syntax,
+    name: Document.Node.Name,
+    spans: List[Command_Span.Span]
+  ) : List[Path] = {
     val dir = name.master_dir_path
     for { span <- spans; file <- span.loaded_files(syntax).files }
       yield (dir + Path.explode(file)).expand
   }
 
-  def pure_files(syntax: Outer_Syntax): List[Path] =
-  {
+  def pure_files(syntax: Outer_Syntax): List[Path] = {
     val pure_dir = Path.explode("~~/src/Pure")
     for {
       (name, theory) <- Thy_Header.ml_roots
       path = (pure_dir + Path.explode(name)).expand
       node_name = Document.Node.Name(path.implode, path.dir.implode, theory)

   def theory_name(qualifier: String, theory: String): String =
     if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
       theory
     else Long_Name.qualify(qualifier, theory)
 
-  def find_theory_node(theory: String): Option[Document.Node.Name] =
-  {
+  def find_theory_node(theory: String): Option[Document.Node.Name] = {
     val thy_file = Path.basic(Long_Name.base_name(theory)).thy
     val session = session_base.theory_qualifier(theory)
     val dirs =
       sessions_structure.get(session) match {
         case Some(info) => info.dirs

       }
     dirs.collectFirst({
       case dir if (dir + thy_file).is_file => file_node(dir + thy_file, theory = theory) })
   }
 
-  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
-  {
+  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name = {
     val theory = theory_name(qualifier, Thy_Header.import_name(s))
     def theory_node = file_node(Path.explode(s).thy, dir = dir, theory = theory)
 
     if (!Thy_Header.is_base_name(s)) theory_node
     else if (session_base.loaded_theory(theory)) loaded_theory_node(theory)

     import_name(session_base.theory_qualifier(name), name.master_dir, s)
 
   def import_name(info: Sessions.Info, s: String): Document.Node.Name =
     import_name(info.name, info.dir.implode, s)
 
-  def find_theory(file: JFile): Option[Document.Node.Name] =
-  {
+  def find_theory(file: JFile): Option[Document.Node.Name] = {
     for {
       qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
       theory_base <- proper_string(Thy_Header.theory_name(file.getName))
       theory = theory_name(qualifier, theory_base)
       theory_node <- find_theory_node(theory)
       if File.eq(theory_node.path.file, file)
     } yield theory_node
   }
 
-  def complete_import_name(context_name: Document.Node.Name, s: String): List[String] =
-  {
+  def complete_import_name(context_name: Document.Node.Name, s: String): List[String] = {
     val context_session = session_base.theory_qualifier(context_name)
     val context_dir =
       try { Some(context_name.master_dir_path) }
       catch { case ERROR(_) => None }
     (for {

       if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
       else Long_Name.qualify(session, theory)
     }).toList.sorted
   }
 
-  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
-  {
+  def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = {
     val path = name.path
     if (path.is_file) using(Scan.byte_reader(path.file))(f)
     else if (name.node == name.theory)
       error("Cannot load theory " + quote(name.theory))
     else error ("Cannot load theory file " + path)
   }
 
-  def check_thy(node_name: Document.Node.Name, reader: Reader[Char],
-    command: Boolean = true, strict: Boolean = true): Document.Node.Header =
-  {
+  def check_thy(
+    node_name: Document.Node.Name,
+    reader: Reader[Char],
+    command: Boolean = true,
+    strict: Boolean = true
+  ): Document.Node.Header = {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
         val header = Thy_Header.read(node_name, reader, command = command, strict = strict)
         val imports =
           header.imports.map({ case (s, pos) =>

   }
 
 
   /* special header */
 
-  def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
-  {
+  def special_header(name: Document.Node.Name): Option[Document.Node.Header] = {
     val imports =
       if (name.theory == Sessions.root_name) List(import_name(name, Sessions.theory_name))
       else if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
       else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
       else Nil

   def dependencies(
       thys: List[(Document.Node.Name, Position.T)],
       progress: Progress = new Progress): Dependencies[Unit] =
     Dependencies.empty[Unit].require_thys((), thys, progress = progress)
 
-  def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
-    : Dependencies[Options] =
-  {
+  def session_dependencies(
+    info: Sessions.Info,
+    progress: Progress = new Progress
+  ) : Dependencies[Options] = {
     info.theories.foldLeft(Dependencies.empty[Options]) {
       case (dependencies, (options, thys)) =>
         dependencies.require_thys(options,
           for { (thy, pos) <- thys } yield (import_name(info, thy), pos),
           progress = progress)
     }
   }
 
-  object Dependencies
-  {
+  object Dependencies {
     def empty[A]: Dependencies[A] = new Dependencies[A](Nil, Map.empty)
 
     private def show_path(names: List[Document.Node.Name]): String =
       names.map(name => quote(name.theory)).mkString(" via ")
 

       else "\n(required by " + show_path(initiators.reverse) + ")"
   }
 
   final class Dependencies[A] private(
     rev_entries: List[Document.Node.Entry],
-    seen: Map[Document.Node.Name, A])
-  {
+    seen: Map[Document.Node.Name, A]
+  ) {
     private def cons(entry: Document.Node.Entry): Dependencies[A] =
       new Dependencies[A](entry :: rev_entries, seen)
 
     def require_thy(adjunct: A,
       thy: (Document.Node.Name, Position.T),
       initiators: List[Document.Node.Name] = Nil,
-      progress: Progress = new Progress): Dependencies[A] =
-    {
+      progress: Progress = new Progress): Dependencies[A] = {
       val (name, pos) = thy
 
       def message: String =
         "The error(s) above occurred for theory " + quote(name.theory) +
           Dependencies.required_by(initiators) + Position.here(pos)

       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
 
-    lazy val theory_graph: Document.Node.Name.Graph[Unit] =
-    {
+    lazy val theory_graph: Document.Node.Name.Graph[Unit] = {
       val regular = theories.toSet
       val irregular =
         (for {
           entry <- entries.iterator
           imp <- entry.header.imports

       theories.zip(
         Par_List.map((e: () => List[Command_Span.Span]) => e(),
           theories.map(name => resources.load_commands(get_syntax(name), name))))
       .filter(p => p._2.nonEmpty)
 
-    def loaded_files(name: Document.Node.Name, spans: List[Command_Span.Span])
-      : (String, List[Path]) =
-    {
+    def loaded_files(
+      name: Document.Node.Name,
+      spans: List[Command_Span.Span]
+    ) : (String, List[Path]) = {
       val theory = name.theory
       val syntax = get_syntax(name)
       val files1 = resources.loaded_files(syntax, name, spans)
       val files2 = if (theory == Thy_Header.PURE) pure_files(syntax) else Nil
       (theory, files1 ::: files2)

       for {
         (name, spans) <- load_commands
         file <- loaded_files(name, spans)._2
       } yield file
 
-    def imported_files: List[Path] =
-    {
+    def imported_files: List[Path] = {
       val base_theories =
         loaded_theories.all_preds(theories.map(_.theory)).
           filter(session_base.loaded_theories.defined)
 
       base_theories.map(theory => session_base.known_theories(theory).name.path) :::