provide session qualifier via resources;
authorwenzelm
Mon Apr 03 16:36:45 2017 +0200 (2017-04-03)
changeset 653599ca34f0407a9
parent 65358 e345e9420109
child 65360 3ff88fece1f6
provide session qualifier via resources;
src/Pure/PIDE/command.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.scala
src/Pure/Tools/build.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Apr 03 14:29:44 2017 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Apr 03 16:36:45 2017 +0200
     1.3 @@ -435,7 +435,7 @@
     1.4        // inlined errors
     1.5        case Thy_Header.THEORY =>
     1.6          val reader = Scan.char_reader(Token.implode(span.content))
     1.7 -        val header = resources.check_thy_reader("", node_name, reader)
     1.8 +        val header = resources.check_thy_reader(node_name, reader)
     1.9          val errors =
    1.10            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    1.11              val msg =
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 03 14:29:44 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 03 16:36:45 2017 +0200
     2.3 @@ -13,25 +13,16 @@
     2.4  import java.io.{File => JFile}
     2.5  
     2.6  
     2.7 -class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
     2.8 +class Resources(
     2.9 +  val session_name: String,
    2.10 +  val base: Sessions.Base,
    2.11 +  val log: Logger = No_Logger)
    2.12  {
    2.13    val thy_info = new Thy_Info(this)
    2.14  
    2.15    def thy_path(path: Path): Path = path.ext("thy")
    2.16  
    2.17  
    2.18 -  /* document node names */
    2.19 -
    2.20 -  def node_name(qualifier: String, raw_path: Path): Document.Node.Name =
    2.21 -  {
    2.22 -    val path = raw_path.expand
    2.23 -    val node = path.implode
    2.24 -    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    2.25 -    val master_dir = if (theory == "") "" else path.dir.implode
    2.26 -    Document.Node.Name(node, master_dir, theory)
    2.27 -  }
    2.28 -
    2.29 -
    2.30    /* file-system operations */
    2.31  
    2.32    def append(dir: String, source_path: Path): String =
    2.33 @@ -76,10 +67,20 @@
    2.34      }
    2.35      else Nil
    2.36  
    2.37 -  def import_name(qualifier: String, master: Document.Node.Name, s: String): Document.Node.Name =
    2.38 +  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
    2.39 +  {
    2.40 +    val path = raw_path.expand
    2.41 +    val node = path.implode
    2.42 +    val qualifier = if (global) "" else session_name
    2.43 +    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
    2.44 +    val master_dir = if (theory == "") "" else path.dir.implode
    2.45 +    Document.Node.Name(node, master_dir, theory)
    2.46 +  }
    2.47 +
    2.48 +  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
    2.49    {
    2.50      val thy1 = Thy_Header.base_name(s)
    2.51 -    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(qualifier, thy1)
    2.52 +    val thy2 = if (Long_Name.is_qualified(thy1)) thy1 else Long_Name.qualify(session_name, thy1)
    2.53      (base.known_theories.get(thy1) orElse
    2.54       base.known_theories.get(thy2) orElse
    2.55       base.known_theories.get(Long_Name.base_name(thy1))) match {
    2.56 @@ -92,7 +93,7 @@
    2.57          else {
    2.58            val node = append(master.master_dir, thy_path(path))
    2.59            val master_dir = append(master.master_dir, path.dir)
    2.60 -          Document.Node.Name(node, master_dir, Long_Name.qualify(qualifier, theory))
    2.61 +          Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
    2.62          }
    2.63      }
    2.64    }
    2.65 @@ -106,9 +107,8 @@
    2.66      try { f(reader) } finally { reader.close }
    2.67    }
    2.68  
    2.69 -  def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
    2.70 -      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
    2.71 -    : Document.Node.Header =
    2.72 +  def check_thy_reader(node_name: Document.Node.Name, reader: Reader[Char],
    2.73 +    start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
    2.74    {
    2.75      if (node_name.is_theory && reader.source.length > 0) {
    2.76        try {
    2.77 @@ -122,7 +122,7 @@
    2.78              Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
    2.79  
    2.80          val imports =
    2.81 -          header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
    2.82 +          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
    2.83          Document.Node.Header(imports, header.keywords, header.abbrevs)
    2.84        }
    2.85        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    2.86 @@ -130,18 +130,18 @@
    2.87      else Document.Node.no_header
    2.88    }
    2.89  
    2.90 -  def check_thy(qualifier: String, name: Document.Node.Name,
    2.91 -      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
    2.92 -    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
    2.93 +  def check_thy(name: Document.Node.Name, start: Token.Pos = Token.Pos.command,
    2.94 +      strict: Boolean = true): Document.Node.Header =
    2.95 +    with_thy_reader(name, check_thy_reader(name, _, start, strict))
    2.96  
    2.97  
    2.98    /* special header */
    2.99  
   2.100    def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
   2.101      if (Thy_Header.is_ml_root(name.theory))
   2.102 -      Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
   2.103 +      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
   2.104      else if (Thy_Header.is_bootstrap(name.theory))
   2.105 -      Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
   2.106 +      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
   2.107      else None
   2.108  
   2.109  
     3.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 03 14:29:44 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 03 16:36:45 2017 +0200
     3.3 @@ -71,12 +71,12 @@
     3.4            if (progress.stopped) throw Exn.Interrupt()
     3.5  
     3.6            try {
     3.7 -            val resources =
     3.8 -              new Resources(
     3.9 -                info.parent match {
    3.10 -                  case None => Base.bootstrap
    3.11 -                  case Some(parent) => deps(parent)
    3.12 -                })
    3.13 +            val parent_base =
    3.14 +              info.parent match {
    3.15 +                case None => Base.bootstrap
    3.16 +                case Some(parent) => deps(parent)
    3.17 +              }
    3.18 +            val resources = new Resources(name, parent_base)
    3.19  
    3.20              if (verbose || list_files) {
    3.21                val groups =
    3.22 @@ -91,10 +91,9 @@
    3.23                  info.theories.flatMap({
    3.24                    case (global, _, thys) =>
    3.25                      thys.map(thy =>
    3.26 -                      (resources.node_name(
    3.27 -                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
    3.28 +                      (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
    3.29                  })
    3.30 -              val thy_deps = resources.thy_info.dependencies(name, root_theories)
    3.31 +              val thy_deps = resources.thy_info.dependencies(root_theories)
    3.32  
    3.33                thy_deps.errors match {
    3.34                  case Nil => thy_deps
    3.35 @@ -103,7 +102,7 @@
    3.36              }
    3.37  
    3.38              val known_theories =
    3.39 -              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    3.40 +              (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    3.41                  val name = dep.name
    3.42                  known.get(name.theory) match {
    3.43                    case Some(name1) if name != name1 =>
    3.44 @@ -142,7 +141,7 @@
    3.45  
    3.46              val session_graph =
    3.47                Present.session_graph(info.parent getOrElse "",
    3.48 -                resources.base.loaded_theories, thy_deps.deps)
    3.49 +                parent_base.loaded_theories, thy_deps.deps)
    3.50  
    3.51              val base =
    3.52                Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
     4.1 --- a/src/Pure/Thy/thy_info.scala	Mon Apr 03 14:29:44 2017 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Mon Apr 03 16:36:45 2017 +0200
     4.3 @@ -104,12 +104,12 @@
     4.4      override def toString: String = deps.toString
     4.5    }
     4.6  
     4.7 -  private def require_thys(session: String, initiators: List[Document.Node.Name],
     4.8 -      required: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
     4.9 -    (required /: thys)(require_thy(session, initiators, _, _))
    4.10 +  private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
    4.11 +      thys: List[(Document.Node.Name, Position.T)]): Dependencies =
    4.12 +    (required /: thys)(require_thy(initiators, _, _))
    4.13  
    4.14 -  private def require_thy(session: String, initiators: List[Document.Node.Name],
    4.15 -      required: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies =
    4.16 +  private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
    4.17 +    thy: (Document.Node.Name, Position.T)): Dependencies =
    4.18    {
    4.19      val (name, require_pos) = thy
    4.20  
    4.21 @@ -123,10 +123,9 @@
    4.22        try {
    4.23          if (initiators.contains(name)) error(cycle_msg(initiators))
    4.24          val header =
    4.25 -          try { resources.check_thy(session, name, Token.Pos.file(name.node)).cat_errors(message) }
    4.26 +          try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
    4.27            catch { case ERROR(msg) => cat_error(msg, message) }
    4.28 -        Thy_Info.Dep(name, header) ::
    4.29 -          require_thys(session, name :: initiators, required1, header.imports)
    4.30 +        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
    4.31        }
    4.32        catch {
    4.33          case e: Throwable =>
    4.34 @@ -135,6 +134,6 @@
    4.35      }
    4.36    }
    4.37  
    4.38 -  def dependencies(session: String, thys: List[(Document.Node.Name, Position.T)]): Dependencies =
    4.39 -    require_thys(session, Nil, Dependencies.empty, thys)
    4.40 +  def dependencies(thys: List[(Document.Node.Name, Position.T)]): Dependencies =
    4.41 +    require_thys(Nil, Dependencies.empty, thys)
    4.42  }
     5.1 --- a/src/Pure/Tools/build.scala	Mon Apr 03 14:29:44 2017 +0200
     5.2 +++ b/src/Pure/Tools/build.scala	Mon Apr 03 16:36:45 2017 +0200
     5.3 @@ -220,7 +220,7 @@
     5.4              ML_Syntax.print_string0(File.platform_path(output))
     5.5  
     5.6          if (pide && !Sessions.pure_name(name)) {
     5.7 -          val resources = new Resources(deps(parent))
     5.8 +          val resources = new Resources(name, deps(parent))
     5.9            val session = new Session(options, resources)
    5.10            val handler = new Handler(progress, session, name)
    5.11            session.init_protocol_handler(handler)
     6.1 --- a/src/Tools/VSCode/src/document_model.scala	Mon Apr 03 14:29:44 2017 +0200
     6.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Apr 03 16:36:45 2017 +0200
     6.3 @@ -73,7 +73,7 @@
     6.4  
     6.5    def node_header: Document.Node.Header =
     6.6      resources.special_header(node_name) getOrElse
     6.7 -      resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
     6.8 +      resources.check_thy_reader(node_name, Scan.char_reader(content.text))
     6.9  
    6.10  
    6.11    /* perspective */
     7.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 14:29:44 2017 +0200
     7.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Apr 03 16:36:45 2017 +0200
     7.3 @@ -42,7 +42,7 @@
     7.4  class VSCode_Resources(
     7.5    val options: Options,
     7.6    base: Sessions.Base,
     7.7 -  log: Logger = No_Logger) extends Resources(base, log)
     7.8 +  log: Logger = No_Logger) extends Resources(session_name = "", base, log)
     7.9  {
    7.10    private val state = Synchronized(VSCode_Resources.State())
    7.11  
    7.12 @@ -165,7 +165,7 @@
    7.13            (for ((_, model) <- st.models.iterator if model.is_theory)
    7.14             yield (model.node_name, Position.none)).toList
    7.15  
    7.16 -        val thy_files = thy_info.dependencies("", thys).deps.map(_.name)
    7.17 +        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
    7.18  
    7.19  
    7.20          /* auxiliary files */
     8.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Apr 03 14:29:44 2017 +0200
     8.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Apr 03 16:36:45 2017 +0200
     8.3 @@ -235,7 +235,7 @@
     8.4                val pending_nodes = for ((node_name, None) <- purged) yield node_name
     8.5                (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
     8.6              }
     8.7 -            val retain = PIDE.resources.thy_info.dependencies("", imports).deps.map(_.name).toSet
     8.8 +            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
     8.9  
    8.10              for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
    8.11                yield edit
    8.12 @@ -331,7 +331,7 @@
    8.13  
    8.14    def node_header: Document.Node.Header =
    8.15      PIDE.resources.special_header(node_name) getOrElse
    8.16 -      PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
    8.17 +      PIDE.resources.check_thy_reader(node_name, Scan.char_reader(content.text), strict = false)
    8.18  
    8.19  
    8.20    /* content */
    8.21 @@ -396,8 +396,7 @@
    8.22  
    8.23      PIDE.resources.special_header(node_name) getOrElse
    8.24        JEdit_Lib.buffer_lock(buffer) {
    8.25 -        PIDE.resources.check_thy_reader(
    8.26 -          "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
    8.27 +        PIDE.resources.check_thy_reader(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
    8.28        }
    8.29    }
    8.30  
     9.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 14:29:44 2017 +0200
     9.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Apr 03 16:36:45 2017 +0200
     9.3 @@ -21,7 +21,7 @@
     9.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     9.5  
     9.6  
     9.7 -class JEdit_Resources(base: Sessions.Base) extends Resources(base)
     9.8 +class JEdit_Resources(base: Sessions.Base) extends Resources(session_name = "", base)
     9.9  {
    9.10    /* document node name */
    9.11  
    10.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 14:29:44 2017 +0200
    10.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 16:36:45 2017 +0200
    10.3 @@ -135,7 +135,7 @@
    10.4            val thys =
    10.5              (for ((node_name, model) <- models.iterator if model.is_theory)
    10.6                yield (node_name, Position.none)).toList
    10.7 -          val thy_files = resources.thy_info.dependencies("", thys).deps.map(_.name)
    10.8 +          val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
    10.9  
   10.10            val aux_files =
   10.11              if (options.bool("jedit_auto_resolve")) {