# HG changeset patch
# User wenzelm
# Date 1421181969 -3600
# Node ID 41f1645a4f63563420f8718b5c09db32133d97ee
# Parent  63c02d05166146b48aa2aed682e86f4ab256f600
some support for PIDE batch session;
clarified Thy_Info.use_thys_options and corresponding protocol command;

diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/PIDE/batch_session.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/batch_session.scala	Tue Jan 13 21:46:09 2015 +0100
@@ -0,0 +1,74 @@
+/*  Title:      Pure/Tools/batch_session.scala
+    Author:     Makarius
+
+PIDE session in batch mode.
+*/
+
+package isabelle
+
+
+import isabelle._
+
+
+object Batch_Session
+{
+  def batch_session(
+    options: Options,
+    verbose: Boolean = false,
+    dirs: List[Path] = Nil,
+    session: String)
+  {
+    val (_, session_tree) =
+      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
+    val session_info = session_tree(session)
+    val parent_session =
+      session_info.parent getOrElse error("No parent session for " + quote(session))
+
+    if (Build.build(options, new Build.Console_Progress(verbose),
+        verbose = verbose, build_heap = true,
+        dirs = dirs, sessions = List(parent_session)) != 0)
+      new RuntimeException
+
+    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
+    val resources =
+    {
+      val content = deps(parent_session)
+      new Resources(content.loaded_theories, content.known_theories, content.syntax)
+    }
+
+    val progress = new Build.Console_Progress(verbose)
+    val result = Future.promise[Unit]
+
+    val prover_session = new Session(resources)
+
+    prover_session.phase_changed +=
+      Session.Consumer[Session.Phase](getClass.getName) {
+        case Session.Ready =>
+          val master_dir = session_info.dir
+          for ((_, thy_options, thy_files) <- session_info.theories) {
+            val id = Document_ID.make().toString
+            prover_session.use_theories(options, id, master_dir, thy_files) // FIXME proper check of result!?
+          }
+        case Session.Inactive | Session.Failed =>
+          result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
+        case Session.Shutdown =>
+          result.fulfill(())
+        case _ =>
+      }
+
+    prover_session.all_messages +=
+      Session.Consumer[Prover.Message](getClass.getName) {
+        case msg: Prover.Output =>
+          msg.properties match {
+            case Markup.Loading_Theory(name) => progress.theory(session, name)
+            case _ =>
+          }
+        case _ =>
+      }
+
+    prover_session.start("Isabelle", List("-r", "-q", parent_session))
+
+    result.join
+  }
+}
+
diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/PIDE/protocol.ML	Tue Jan 13 21:46:09 2015 +0100
@@ -112,12 +112,12 @@
 
 val _ =
   Isabelle_Process.protocol_command "use_theories"
-    (fn id :: master_dir :: thys =>
+    (fn options_yxml :: id :: master_dir :: thys =>
       let
+        val options = Options.decode (YXML.parse_body options_yxml);
         val result =
           Exn.capture (fn () =>
-            Thy_Info.use_theories
-              {document = false, last_timing = K NONE, master_dir = Path.explode master_dir}
+            Thy_Info.use_thys_options (K NONE) (Path.explode master_dir) options
               (map (rpair Position.none) thys)) ();
         val ok =
           (case result of
diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Jan 13 21:46:09 2015 +0100
@@ -470,6 +470,8 @@
 
   /* use_theories */
 
-  def use_theories(id: String, master_dir: Path, thys: List[Path]): Unit =
-    protocol_command("use_theories", (id :: master_dir.implode :: thys.map(_.implode)): _*)
+  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path]): Unit =
+    protocol_command("use_theories",
+      (YXML.string_of_body(Options.encode(options)) ::
+        id :: master_dir.implode :: thys.map(_.implode)): _*)
 }
diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Jan 13 21:46:09 2015 +0100
@@ -63,6 +63,7 @@
   case object Caret_Focus
   case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
   case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
+  case class Use_Theories(options: Options, id: String, master_dir: Path, thys: List[Path])
   case class Commands_Changed(
     assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
 
@@ -553,6 +554,9 @@
             prover.get.dialog_result(serial, result)
             handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
 
+          case Session.Use_Theories(options, id, master_dir, thys) if prover.defined =>
+            prover.get.use_theories(options, id, master_dir, thys)
+
           case Protocol_Command(name, args) if prover.defined =>
             prover.get.protocol_command(name, args:_*)
 
@@ -615,4 +619,7 @@
 
   def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
   { manager.send(Session.Dialog_Result(id, serial, result)) }
+
+  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path])
+  { manager.send(Session.Use_Theories(options, id, master_dir, thys)) }
 }
diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/Thy/thy_info.ML	Tue Jan 13 21:46:09 2015 +0100
@@ -12,11 +12,10 @@
   val get_theory: string -> theory
   val master_directory: string -> Path.T
   val remove_thy: string -> unit
-  val use_theories:
-    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
-    (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
+  val use_thys_options: (Toplevel.transition -> Time.time option) -> Path.T ->
+    Options.T -> (string * Position.T) list -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
@@ -343,6 +342,19 @@
 val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
 val use_thy = use_thys o single;
 
+fun use_thys_options last_timing master_dir options thys =
+  (Options.set_default options;
+    (use_theories {
+        document = Present.document_enabled (Options.string options "document"),
+        last_timing = last_timing,
+        master_dir = master_dir}
+      |> Unsynchronized.setmp print_mode
+          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
+      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
+      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
+      |> Multithreading.max_threads_setmp (Options.int options "threads")
+      |> Unsynchronized.setmp Future.ML_statistics true) thys);
+
 
 (* toplevel scripting -- without maintaining database *)
 
diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/Tools/build.ML	Tue Jan 13 21:46:09 2015 +0100
@@ -97,33 +97,17 @@
 
 (* build *)
 
-local
-
-fun use_theories last_timing options =
-  Thy_Info.use_theories {
-      document = Present.document_enabled (Options.string options "document"),
-      last_timing = last_timing,
-      master_dir = Path.current}
-    |> Unsynchronized.setmp print_mode
-        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
-    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
-    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
-    |> Multithreading.max_threads_setmp (Options.int options "threads")
-    |> Unsynchronized.setmp Future.ML_statistics true;
-
-fun use_theories_condition last_timing (options, thys) =
+fun use_theories last_timing master_dir (options, thys) =
   let val condition = space_explode "," (Options.string options "condition") in
     (case filter_out (can getenv_strict) condition of
       [] =>
-        (Options.set_default options;
-         use_theories last_timing options (map (rpair Position.none) thys))
+        Thy_Info.use_thys_options last_timing master_dir options
+          (map (rpair Position.none) thys)
     | conds =>
         Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
           " (undefined " ^ commas conds ^ ")\n"))
   end;
 
-in
-
 fun build args_file = Command_Line.tool0 (fn () =>
     let
       val _ = SHA1_Samples.test ();
@@ -156,7 +140,7 @@
 
       val res1 =
         theories |>
-          (List.app (use_theories_condition last_timing)
+          (List.app (use_theories last_timing Path.current)
             |> session_timing name verbose
             |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
             |> Multithreading.max_threads_setmp (Options.int options "threads")
@@ -169,5 +153,3 @@
     in () end);
 
 end;
-
-end;
diff -r 63c02d051661 -r 41f1645a4f63 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Jan 11 21:06:47 2015 +0100
+++ b/src/Pure/build-jars	Tue Jan 13 21:46:09 2015 +0100
@@ -55,6 +55,7 @@
   Isar/parse.scala
   Isar/token.scala
   ML/ml_lex.scala
+  PIDE/batch_session.scala
   PIDE/command.scala
   PIDE/command_span.scala
   PIDE/document.scala