provide session base for "isabelle build" and "isabelle console" ML process;
authorwenzelm
Fri Apr 07 19:35:39 2017 +0200 (2017-04-07 ago)
changeset 654314a3e6cda3b94
parent 65430 4433d189a77d
child 65432 d938705819bb
provide session base for "isabelle build" and "isabelle console" ML process;
src/Pure/ML/ml_syntax.scala
src/Pure/PIDE/resources.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/Tools/ml_console.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/ML/ml_syntax.scala	Fri Apr 07 18:26:30 2017 +0200
     1.2 +++ b/src/Pure/ML/ml_syntax.scala	Fri Apr 07 19:35:39 2017 +0200
     1.3 @@ -46,6 +46,12 @@
     1.4      quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
     1.5  
     1.6  
     1.7 +  /* pair */
     1.8 +
     1.9 +  def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
    1.10 +    "(" + f(pair._1) + ", " + g(pair._2) + ")"
    1.11 +
    1.12 +
    1.13    /* list */
    1.14  
    1.15    def print_list[A](f: A => String)(list: List[A]): String =
     2.1 --- a/src/Pure/PIDE/resources.ML	Fri Apr 07 18:26:30 2017 +0200
     2.2 +++ b/src/Pure/PIDE/resources.ML	Fri Apr 07 19:35:39 2017 +0200
     2.3 @@ -6,6 +6,9 @@
     2.4  
     2.5  signature RESOURCES =
     2.6  sig
     2.7 +  val set_session_base: {known_theories: (string * string) list} -> unit
     2.8 +  val reset_session_base: unit -> unit
     2.9 +  val known_theory: string -> Path.T option
    2.10    val master_directory: theory -> Path.T
    2.11    val imports_of: theory -> (string * Position.T) list
    2.12    val thy_path: Path.T -> Path.T
    2.13 @@ -25,6 +28,23 @@
    2.14  structure Resources: RESOURCES =
    2.15  struct
    2.16  
    2.17 +(* session base *)
    2.18 +
    2.19 +val global_session_base =
    2.20 +  Synchronized.var "Sessions.base"
    2.21 +    ({known_theories = Symtab.empty: Path.T Symtab.table});
    2.22 +
    2.23 +fun set_session_base {known_theories} =
    2.24 +  Synchronized.change global_session_base
    2.25 +    (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    2.26 +
    2.27 +fun reset_session_base () =
    2.28 +  set_session_base {known_theories = []};
    2.29 +
    2.30 +fun known_theory name =
    2.31 +  Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
    2.32 +
    2.33 +
    2.34  (* manage source files *)
    2.35  
    2.36  type files =
     3.1 --- a/src/Pure/Tools/build.ML	Fri Apr 07 18:26:30 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.ML	Fri Apr 07 19:35:39 2017 +0200
     3.3 @@ -144,30 +144,37 @@
     3.4    chapter: string,
     3.5    name: string,
     3.6    master_dir: Path.T,
     3.7 -  theories: (Options.T * (string * Position.T) list) list};
     3.8 +  theories: (Options.T * (string * Position.T) list) list,
     3.9 +  known_theories: (string * string) list};
    3.10  
    3.11  fun decode_args yxml =
    3.12    let
    3.13      open XML.Decode;
    3.14      val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
    3.15 -      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) =
    3.16 +      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
    3.17 +      (theories, known_theories)))))))))))) =
    3.18        pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
    3.19          (pair (list (pair string string)) (pair string (pair string (pair string (pair string
    3.20 -          (pair string (((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))))
    3.21 +          (pair string
    3.22 +            (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
    3.23 +              (list (pair string string)))))))))))))
    3.24        (YXML.parse_body yxml);
    3.25    in
    3.26      Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
    3.27        verbose = verbose, browser_info = Path.explode browser_info,
    3.28        document_files = map (apply2 Path.explode) document_files,
    3.29        graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
    3.30 -      name = name, master_dir = Path.explode master_dir, theories = theories}
    3.31 +      name = name, master_dir = Path.explode master_dir, theories = theories,
    3.32 +      known_theories = known_theories}
    3.33    end;
    3.34  
    3.35  fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
    3.36 -    document_files, graph_file, parent_name, chapter, name, master_dir, theories}) =
    3.37 +    document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
    3.38    let
    3.39      val symbols = HTML.make_symbols symbol_codes;
    3.40  
    3.41 +    val _ = Resources.set_session_base {known_theories = known_theories};
    3.42 +
    3.43      val _ =
    3.44        Session.init
    3.45          symbols
    3.46 @@ -191,6 +198,8 @@
    3.47            |> session_timing name verbose
    3.48            |> Exn.capture);
    3.49      val res2 = Exn.capture Session.finish ();
    3.50 +
    3.51 +    val _ = Resources.reset_session_base ();
    3.52      val _ = Par_Exn.release_all [res1, res2];
    3.53    in () end;
    3.54  
     4.1 --- a/src/Pure/Tools/build.scala	Fri Apr 07 18:26:30 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 19:35:39 2017 +0200
     4.3 @@ -197,6 +197,10 @@
     4.4        Future.thread("build") {
     4.5          val parent = info.parent.getOrElse("")
     4.6  
     4.7 +        val known_theories =
     4.8 +          for ((theory, node_name) <- deps(name).known_theories.toList)
     4.9 +            yield (theory, node_name.node)
    4.10 +
    4.11          val args_yxml =
    4.12            YXML.string_of_body(
    4.13              {
    4.14 @@ -204,11 +208,13 @@
    4.15                pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
    4.16                  pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    4.17                  pair(string, pair(string, pair(string, pair(Path.encode,
    4.18 -                list(pair(Options.encode, list(string))))))))))))))(
    4.19 +                pair(list(pair(Options.encode, list(string))),
    4.20 +                list(pair(string, string))))))))))))))(
    4.21                (Symbol.codes, (command_timings, (do_output, (verbose,
    4.22                  (store.browser_info, (info.document_files, (File.standard_path(graph_file),
    4.23                  (parent, (info.chapter, (name, (Path.current,
    4.24 -                info.theories))))))))))))
    4.25 +                (info.theories,
    4.26 +                known_theories)))))))))))))
    4.27              })
    4.28  
    4.29          val env =
     5.1 --- a/src/Pure/Tools/ml_console.scala	Fri Apr 07 18:26:30 2017 +0200
     5.2 +++ b/src/Pure/Tools/ml_console.scala	Fri Apr 07 19:35:39 2017 +0200
     5.3 @@ -72,7 +72,10 @@
     5.4        val process =
     5.5          ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
     5.6            modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
     5.7 -          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
     5.8 +          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
     5.9 +          session_base =
    5.10 +            if (raw_ml_system) None
    5.11 +            else Some(Sessions.session_base(options, logic, dirs)))
    5.12        val process_output = Future.thread[Unit]("process_output") {
    5.13          try {
    5.14            var result = new StringBuilder(100)
     6.1 --- a/src/Pure/Tools/ml_process.scala	Fri Apr 07 18:26:30 2017 +0200
     6.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 19:35:39 2017 +0200
     6.3 @@ -24,6 +24,7 @@
     6.4      cleanup: () => Unit = () => (),
     6.5      channel: Option[System_Channel] = None,
     6.6      sessions: Option[Sessions.T] = None,
     6.7 +    session_base: Option[Sessions.Base] = None,
     6.8      store: Sessions.Store = Sessions.store()): Bash.Process =
     6.9    {
    6.10      val logic_name = Isabelle_System.default_logic(logic)
    6.11 @@ -89,6 +90,21 @@
    6.12      val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
    6.13      val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
    6.14  
    6.15 +    // session base
    6.16 +    val eval_session_base =
    6.17 +      session_base match {
    6.18 +        case None => Nil
    6.19 +        case Some(base) =>
    6.20 +          val known_theories =
    6.21 +            for ((theory, node_name) <- base.known_theories.toList)
    6.22 +              yield (theory, node_name.node)
    6.23 +          List("Resources.set_session_base {known_theories = " +
    6.24 +            ML_Syntax.print_list(
    6.25 +              ML_Syntax.print_pair(
    6.26 +                ML_Syntax.print_string, ML_Syntax.print_string))(known_theories) + "}")
    6.27 +      }
    6.28 +
    6.29 +    // process
    6.30      val eval_process =
    6.31        if (heaps.isEmpty)
    6.32          List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
    6.33 @@ -114,7 +130,7 @@
    6.34      // bash
    6.35      val bash_args =
    6.36        ml_runtime_options :::
    6.37 -      (eval_init ::: eval_modes ::: eval_options ::: eval_process).
    6.38 +      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
    6.39          map(eval => List("--eval", eval)).flatten ::: args
    6.40  
    6.41      Bash.process(