more session_base information in ML;
authorwenzelm
Sat Apr 08 20:56:41 2017 +0200 (2017-04-08)
changeset 654419425e4d8bdb6
parent 65440 fd147f56d9be
child 65442 1ca6d8a2a00d
more session_base information in ML;
tuned signature;
src/Pure/PIDE/resources.ML
src/Pure/PIDE/resources.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Pure/PIDE/resources.ML	Sat Apr 08 12:47:34 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 20:56:41 2017 +0200
     1.3 @@ -6,8 +6,15 @@
     1.4  
     1.5  signature RESOURCES =
     1.6  sig
     1.7 -  val set_session_base: {known_theories: (string * string) list} -> unit
     1.8 +  val set_session_base:
     1.9 +    {default_qualifier: string,
    1.10 +     global_theories: string list,
    1.11 +     loaded_theories: (string * string) list,
    1.12 +     known_theories: (string * string) list} -> unit
    1.13    val reset_session_base: unit -> unit
    1.14 +  val default_qualifier: unit -> string
    1.15 +  val global_theory: string -> bool
    1.16 +  val loaded_theory: string -> Path.T option
    1.17    val known_theory: string -> Path.T option
    1.18    val master_directory: theory -> Path.T
    1.19    val imports_of: theory -> (string * Position.T) list
    1.20 @@ -30,19 +37,32 @@
    1.21  
    1.22  (* session base *)
    1.23  
    1.24 -val global_session_base =
    1.25 -  Synchronized.var "Sessions.base"
    1.26 -    ({known_theories = Symtab.empty: Path.T Symtab.table});
    1.27 +val init_session_base =
    1.28 +  {default_qualifier = "",
    1.29 +   global_theories = Symtab.make_set [],
    1.30 +   loaded_theories = Symtab.empty: Path.T Symtab.table,
    1.31 +   known_theories = Symtab.empty: Path.T Symtab.table};
    1.32  
    1.33 -fun set_session_base {known_theories} =
    1.34 +val global_session_base =
    1.35 +  Synchronized.var "Sessions.base" init_session_base;
    1.36 +
    1.37 +fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
    1.38    Synchronized.change global_session_base
    1.39 -    (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.40 +    (fn _ =>
    1.41 +      {default_qualifier = default_qualifier,
    1.42 +       global_theories = Symtab.make_set global_theories,
    1.43 +       loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
    1.44 +       known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.45  
    1.46  fun reset_session_base () =
    1.47 -  set_session_base {known_theories = []};
    1.48 +  Synchronized.change global_session_base (K init_session_base);
    1.49 +
    1.50 +fun get_session_base f = f (Synchronized.value global_session_base);
    1.51  
    1.52 -fun known_theory name =
    1.53 -  Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
    1.54 +fun default_qualifier () = get_session_base #default_qualifier;
    1.55 +fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
    1.56 +fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    1.57 +fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    1.58  
    1.59  
    1.60  (* manage source files *)
     2.1 --- a/src/Pure/PIDE/resources.scala	Sat Apr 08 12:47:34 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Sat Apr 08 20:56:41 2017 +0200
     2.3 @@ -14,8 +14,8 @@
     2.4  
     2.5  
     2.6  class Resources(
     2.7 -  val session_name: String,
     2.8    val session_base: Sessions.Base,
     2.9 +  val default_qualifier: String = "",
    2.10    val log: Logger = No_Logger)
    2.11  {
    2.12    val thy_info = new Thy_Info(this)
    2.13 @@ -72,7 +72,7 @@
    2.14      val theory0 = Thy_Header.base_name(s)
    2.15      val theory =
    2.16        if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
    2.17 -      else Long_Name.qualify(session_name, theory0)
    2.18 +      else Long_Name.qualify(default_qualifier, theory0)
    2.19  
    2.20      session_base.loaded_theories.get(theory) orElse
    2.21      session_base.loaded_theories.get(theory0) orElse
     3.1 --- a/src/Pure/Thy/sessions.scala	Sat Apr 08 12:47:34 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Sat Apr 08 20:56:41 2017 +0200
     3.3 @@ -58,6 +58,10 @@
     3.4      def loaded_theory(name: Document.Node.Name): Boolean =
     3.5        loaded_theories.isDefinedAt(name.theory)
     3.6  
     3.7 +    def dest_loaded_theories: List[(String, String)] =
     3.8 +      for ((theory, node_name) <- loaded_theories.toList)
     3.9 +        yield (theory, node_name.node)
    3.10 +
    3.11      def dest_known_theories: List[(String, String)] =
    3.12        for ((theory, node_name) <- known_theories.toList)
    3.13          yield (theory, node_name.node)
    3.14 @@ -91,7 +95,7 @@
    3.15                case None => Base.bootstrap
    3.16                case Some(parent) => sessions(parent)
    3.17              }
    3.18 -          val resources = new Resources(session_name, parent_base)
    3.19 +          val resources = new Resources(parent_base, default_qualifier = session_name)
    3.20  
    3.21            if (verbose || list_files) {
    3.22              val groups =
     4.1 --- a/src/Pure/Tools/build.ML	Sat Apr 08 12:47:34 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.ML	Sat Apr 08 20:56:41 2017 +0200
     4.3 @@ -145,6 +145,8 @@
     4.4    name: string,
     4.5    master_dir: Path.T,
     4.6    theories: (Options.T * (string * Position.T) list) list,
     4.7 +  global_theories: string list,
     4.8 +  loaded_theories: (string * string) list,
     4.9    known_theories: (string * string) list};
    4.10  
    4.11  fun decode_args yxml =
    4.12 @@ -152,12 +154,13 @@
    4.13      open XML.Decode;
    4.14      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    4.15        (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
    4.16 -      (theories, known_theories)))))))))))) =
    4.17 +      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
    4.18        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    4.19          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    4.20            (pair string
    4.21              (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
    4.22 -              (list (pair string string)))))))))))))
    4.23 +              (pair (list string)
    4.24 +                (pair (list (pair string string)) (list (pair string string)))))))))))))))
    4.25        (YXML.parse_body yxml);
    4.26    in
    4.27      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    4.28 @@ -165,15 +168,22 @@
    4.29        document_files = map (apply2 Path.explode) document_files,
    4.30        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
    4.31        name = name, master_dir = Path.explode master_dir, theories = theories,
    4.32 +      global_theories = global_theories, loaded_theories = loaded_theories,
    4.33        known_theories = known_theories}
    4.34    end;
    4.35  
    4.36  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
    4.37 -    document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
    4.38 +    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
    4.39 +    global_theories, loaded_theories, known_theories}) =
    4.40    let
    4.41      val symbols = HTML.make_symbols symbol_codes;
    4.42  
    4.43 -    val _ = Resources.set_session_base {known_theories = known_theories};
    4.44 +    val _ =
    4.45 +      Resources.set_session_base
    4.46 +        {default_qualifier = name,
    4.47 +         global_theories = global_theories,
    4.48 +         loaded_theories = loaded_theories,
    4.49 +         known_theories = known_theories};
    4.50  
    4.51      val _ =
    4.52        Session.init
     5.1 --- a/src/Pure/Tools/build.scala	Sat Apr 08 12:47:34 2017 +0200
     5.2 +++ b/src/Pure/Tools/build.scala	Sat Apr 08 20:56:41 2017 +0200
     5.3 @@ -196,7 +196,7 @@
     5.4      private val future_result: Future[Process_Result] =
     5.5        Future.thread("build") {
     5.6          val parent = info.parent.getOrElse("")
     5.7 -
     5.8 +        val base = deps(name)
     5.9          val args_yxml =
    5.10            YXML.string_of_body(
    5.11              {
    5.12 @@ -205,12 +205,14 @@
    5.13                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    5.14                  pair(string, pair(string, pair(string, pair(Path.encode,
    5.15                  pair(list(pair(Options.encode, list(string))),
    5.16 -                list(pair(string, string))))))))))))))(
    5.17 +                pair(list(string),
    5.18 +                pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
    5.19                (Symbol.codes, (command_timings, (do_output, (verbose,
    5.20                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    5.21                  (parent, (info.chapter, (name, (Path.current,
    5.22                  (info.theories,
    5.23 -                deps(name).dest_known_theories)))))))))))))
    5.24 +                (base.global_theories.toList,
    5.25 +                (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
    5.26              })
    5.27  
    5.28          val env =
    5.29 @@ -222,7 +224,7 @@
    5.30              ML_Syntax.print_string0(File.platform_path(output))
    5.31  
    5.32          if (pide && !Sessions.is_pure(name)) {
    5.33 -          val resources = new Resources(name, deps(parent))
    5.34 +          val resources = new Resources(deps(parent), default_qualifier = name)
    5.35            val session = new Session(options, resources)
    5.36            val handler = new Handler(progress, session, name)
    5.37            session.init_protocol_handler(handler)
     6.1 --- a/src/Pure/Tools/ml_process.scala	Sat Apr 08 12:47:34 2017 +0200
     6.2 +++ b/src/Pure/Tools/ml_process.scala	Sat Apr 08 20:56:41 2017 +0200
     6.3 @@ -95,10 +95,15 @@
     6.4        session_base match {
     6.5          case None => Nil
     6.6          case Some(base) =>
     6.7 -          List("Resources.set_session_base {known_theories = " +
     6.8 +          def print_table(table: List[(String, String)]): String =
     6.9              ML_Syntax.print_list(
    6.10                ML_Syntax.print_pair(
    6.11 -                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
    6.12 +                ML_Syntax.print_string, ML_Syntax.print_string))(table)
    6.13 +          List("Resources.set_session_base {default_qualifier = \"\"" +
    6.14 +            ", global_theories = " +
    6.15 +              ML_Syntax.print_list(ML_Syntax.print_string)(base.global_theories.toList) +
    6.16 +            ", loaded_theories = " + print_table(base.dest_loaded_theories) +
    6.17 +            ", known_theories = " + print_table(base.dest_known_theories) + "}")
    6.18        }
    6.19  
    6.20      // process
     7.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Apr 08 12:47:34 2017 +0200
     7.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Apr 08 20:56:41 2017 +0200
     7.3 @@ -43,7 +43,7 @@
     7.4      val options: Options,
     7.5      session_base: Sessions.Base,
     7.6      log: Logger = No_Logger)
     7.7 -  extends Resources(session_name = "", session_base, log)
     7.8 +  extends Resources(session_base, log = log)
     7.9  {
    7.10    private val state = Synchronized(VSCode_Resources.State())
    7.11  
     8.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sat Apr 08 12:47:34 2017 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sat Apr 08 20:56:41 2017 +0200
     8.3 @@ -21,8 +21,7 @@
     8.4  import org.gjt.sp.jedit.bufferio.BufferIORequest
     8.5  
     8.6  
     8.7 -class JEdit_Resources(session_base: Sessions.Base)
     8.8 -  extends Resources(session_name = "", session_base)
     8.9 +class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
    8.10  {
    8.11    /* document node name */
    8.12