src/Pure/PIDE/resources.scala
changeset 65489 f3076367f4a8
parent 65488 331f09d9535e
child 65494 88e6442c3150
equal deleted inserted replaced
65488:331f09d9535e 65489:f3076367f4a8
    91             val master_dir = append(dir, path.dir)
    91             val master_dir = append(dir, path.dir)
    92             Document.Node.Name(node, master_dir, theory)
    92             Document.Node.Name(node, master_dir, theory)
    93         }
    93         }
    94     }
    94     }
    95 
    95 
       
    96   def import_name(node_name: Document.Node.Name, s: String): Document.Node.Name =
       
    97     import_name(theory_qualifier(node_name), node_name.master_dir, s)
       
    98 
    96   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    99   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    97   {
   100   {
    98     val path = Path.explode(name.node)
   101     val path = Path.explode(name.node)
    99     if (!path.is_file) error("No such file: " + path.toString)
   102     if (!path.is_file) error("No such file: " + path.toString)
   100 
   103 
   114         if (base_name != name)
   117         if (base_name != name)
   115           error("Bad theory name " + quote(name) +
   118           error("Bad theory name " + quote(name) +
   116             " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
   119             " for file " + thy_path(Path.basic(base_name)) + Position.here(pos) +
   117             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
   120             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
   118 
   121 
   119         val imports =
   122         val imports = header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
   120           header.imports.map({ case (s, pos) =>
       
   121             (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
       
   122         Document.Node.Header(imports, header.keywords, header.abbrevs)
   123         Document.Node.Header(imports, header.keywords, header.abbrevs)
   123       }
   124       }
   124       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   125       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   125     }
   126     }
   126     else Document.Node.no_header
   127     else Document.Node.no_header
   133 
   134 
   134   /* special header */
   135   /* special header */
   135 
   136 
   136   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   137   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   137   {
   138   {
   138     val qualifier = theory_qualifier(name)
       
   139     val dir = name.master_dir
       
   140 
       
   141     val imports =
   139     val imports =
   142       if (Thy_Header.is_ml_root(name.theory))
   140       if (Thy_Header.is_ml_root(name.theory)) List(import_name(name, Thy_Header.ML_BOOTSTRAP))
   143         List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
   141       else if (Thy_Header.is_bootstrap(name.theory)) List(import_name(name, Thy_Header.PURE))
   144       else if (Thy_Header.is_bootstrap(name.theory))
       
   145         List(import_name(qualifier, dir, Thy_Header.PURE))
       
   146       else Nil
   142       else Nil
   147 
       
   148     if (imports.isEmpty) None
   143     if (imports.isEmpty) None
   149     else Some(Document.Node.Header(imports.map((_, Position.none))))
   144     else Some(Document.Node.Header(imports.map((_, Position.none))))
   150   }
   145   }
   151 
   146 
   152 
   147