some support for PIDE batch session;
authorwenzelm
Tue Jan 13 21:46:09 2015 +0100 (2015-01-13)
changeset 5936241f1645a4f63
parent 59352 63c02d051661
child 59363 4660b0409096
some support for PIDE batch session;
clarified Thy_Info.use_thys_options and corresponding protocol command;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Tue Jan 13 21:46:09 2015 +0100
     1.3 @@ -0,0 +1,74 @@
     1.4 +/*  Title:      Pure/Tools/batch_session.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +PIDE session in batch mode.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +
    1.16 +object Batch_Session
    1.17 +{
    1.18 +  def batch_session(
    1.19 +    options: Options,
    1.20 +    verbose: Boolean = false,
    1.21 +    dirs: List[Path] = Nil,
    1.22 +    session: String)
    1.23 +  {
    1.24 +    val (_, session_tree) =
    1.25 +      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
    1.26 +    val session_info = session_tree(session)
    1.27 +    val parent_session =
    1.28 +      session_info.parent getOrElse error("No parent session for " + quote(session))
    1.29 +
    1.30 +    if (Build.build(options, new Build.Console_Progress(verbose),
    1.31 +        verbose = verbose, build_heap = true,
    1.32 +        dirs = dirs, sessions = List(parent_session)) != 0)
    1.33 +      new RuntimeException
    1.34 +
    1.35 +    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
    1.36 +    val resources =
    1.37 +    {
    1.38 +      val content = deps(parent_session)
    1.39 +      new Resources(content.loaded_theories, content.known_theories, content.syntax)
    1.40 +    }
    1.41 +
    1.42 +    val progress = new Build.Console_Progress(verbose)
    1.43 +    val result = Future.promise[Unit]
    1.44 +
    1.45 +    val prover_session = new Session(resources)
    1.46 +
    1.47 +    prover_session.phase_changed +=
    1.48 +      Session.Consumer[Session.Phase](getClass.getName) {
    1.49 +        case Session.Ready =>
    1.50 +          val master_dir = session_info.dir
    1.51 +          for ((_, thy_options, thy_files) <- session_info.theories) {
    1.52 +            val id = Document_ID.make().toString
    1.53 +            prover_session.use_theories(options, id, master_dir, thy_files) // FIXME proper check of result!?
    1.54 +          }
    1.55 +        case Session.Inactive | Session.Failed =>
    1.56 +          result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    1.57 +        case Session.Shutdown =>
    1.58 +          result.fulfill(())
    1.59 +        case _ =>
    1.60 +      }
    1.61 +
    1.62 +    prover_session.all_messages +=
    1.63 +      Session.Consumer[Prover.Message](getClass.getName) {
    1.64 +        case msg: Prover.Output =>
    1.65 +          msg.properties match {
    1.66 +            case Markup.Loading_Theory(name) => progress.theory(session, name)
    1.67 +            case _ =>
    1.68 +          }
    1.69 +        case _ =>
    1.70 +      }
    1.71 +
    1.72 +    prover_session.start("Isabelle", List("-r", "-q", parent_session))
    1.73 +
    1.74 +    result.join
    1.75 +  }
    1.76 +}
    1.77 +
     2.1 --- a/src/Pure/PIDE/protocol.ML	Sun Jan 11 21:06:47 2015 +0100
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Tue Jan 13 21:46:09 2015 +0100
     2.3 @@ -112,12 +112,12 @@
     2.4  
     2.5  val _ =
     2.6    Isabelle_Process.protocol_command "use_theories"
     2.7 -    (fn id :: master_dir :: thys =>
     2.8 +    (fn options_yxml :: id :: master_dir :: thys =>
     2.9        let
    2.10 +        val options = Options.decode (YXML.parse_body options_yxml);
    2.11          val result =
    2.12            Exn.capture (fn () =>
    2.13 -            Thy_Info.use_theories
    2.14 -              {document = false, last_timing = K NONE, master_dir = Path.explode master_dir}
    2.15 +            Thy_Info.use_thys_options (K NONE) (Path.explode master_dir) options
    2.16                (map (rpair Position.none) thys)) ();
    2.17          val ok =
    2.18            (case result of
     3.1 --- a/src/Pure/PIDE/protocol.scala	Sun Jan 11 21:06:47 2015 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Jan 13 21:46:09 2015 +0100
     3.3 @@ -470,6 +470,8 @@
     3.4  
     3.5    /* use_theories */
     3.6  
     3.7 -  def use_theories(id: String, master_dir: Path, thys: List[Path]): Unit =
     3.8 -    protocol_command("use_theories", (id :: master_dir.implode :: thys.map(_.implode)): _*)
     3.9 +  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path]): Unit =
    3.10 +    protocol_command("use_theories",
    3.11 +      (YXML.string_of_body(Options.encode(options)) ::
    3.12 +        id :: master_dir.implode :: thys.map(_.implode)): _*)
    3.13  }
     4.1 --- a/src/Pure/PIDE/session.scala	Sun Jan 11 21:06:47 2015 +0100
     4.2 +++ b/src/Pure/PIDE/session.scala	Tue Jan 13 21:46:09 2015 +0100
     4.3 @@ -63,6 +63,7 @@
     4.4    case object Caret_Focus
     4.5    case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     4.6    case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
     4.7 +  case class Use_Theories(options: Options, id: String, master_dir: Path, thys: List[Path])
     4.8    case class Commands_Changed(
     4.9      assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    4.10  
    4.11 @@ -553,6 +554,9 @@
    4.12              prover.get.dialog_result(serial, result)
    4.13              handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
    4.14  
    4.15 +          case Session.Use_Theories(options, id, master_dir, thys) if prover.defined =>
    4.16 +            prover.get.use_theories(options, id, master_dir, thys)
    4.17 +
    4.18            case Protocol_Command(name, args) if prover.defined =>
    4.19              prover.get.protocol_command(name, args:_*)
    4.20  
    4.21 @@ -615,4 +619,7 @@
    4.22  
    4.23    def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
    4.24    { manager.send(Session.Dialog_Result(id, serial, result)) }
    4.25 +
    4.26 +  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path])
    4.27 +  { manager.send(Session.Use_Theories(options, id, master_dir, thys)) }
    4.28  }
     5.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jan 11 21:06:47 2015 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Jan 13 21:46:09 2015 +0100
     5.3 @@ -12,11 +12,10 @@
     5.4    val get_theory: string -> theory
     5.5    val master_directory: string -> Path.T
     5.6    val remove_thy: string -> unit
     5.7 -  val use_theories:
     5.8 -    {document: bool, last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} ->
     5.9 -    (string * Position.T) list -> unit
    5.10    val use_thys: (string * Position.T) list -> unit
    5.11    val use_thy: string * Position.T -> unit
    5.12 +  val use_thys_options: (Toplevel.transition -> Time.time option) -> Path.T ->
    5.13 +    Options.T -> (string * Position.T) list -> unit
    5.14    val script_thy: Position.T -> string -> theory -> theory
    5.15    val register_thy: theory -> unit
    5.16    val finish: unit -> unit
    5.17 @@ -343,6 +342,19 @@
    5.18  val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
    5.19  val use_thy = use_thys o single;
    5.20  
    5.21 +fun use_thys_options last_timing master_dir options thys =
    5.22 +  (Options.set_default options;
    5.23 +    (use_theories {
    5.24 +        document = Present.document_enabled (Options.string options "document"),
    5.25 +        last_timing = last_timing,
    5.26 +        master_dir = master_dir}
    5.27 +      |> Unsynchronized.setmp print_mode
    5.28 +          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    5.29 +      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    5.30 +      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    5.31 +      |> Multithreading.max_threads_setmp (Options.int options "threads")
    5.32 +      |> Unsynchronized.setmp Future.ML_statistics true) thys);
    5.33 +
    5.34  
    5.35  (* toplevel scripting -- without maintaining database *)
    5.36  
     6.1 --- a/src/Pure/Tools/build.ML	Sun Jan 11 21:06:47 2015 +0100
     6.2 +++ b/src/Pure/Tools/build.ML	Tue Jan 13 21:46:09 2015 +0100
     6.3 @@ -97,33 +97,17 @@
     6.4  
     6.5  (* build *)
     6.6  
     6.7 -local
     6.8 -
     6.9 -fun use_theories last_timing options =
    6.10 -  Thy_Info.use_theories {
    6.11 -      document = Present.document_enabled (Options.string options "document"),
    6.12 -      last_timing = last_timing,
    6.13 -      master_dir = Path.current}
    6.14 -    |> Unsynchronized.setmp print_mode
    6.15 -        (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    6.16 -    |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    6.17 -    |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    6.18 -    |> Multithreading.max_threads_setmp (Options.int options "threads")
    6.19 -    |> Unsynchronized.setmp Future.ML_statistics true;
    6.20 -
    6.21 -fun use_theories_condition last_timing (options, thys) =
    6.22 +fun use_theories last_timing master_dir (options, thys) =
    6.23    let val condition = space_explode "," (Options.string options "condition") in
    6.24      (case filter_out (can getenv_strict) condition of
    6.25        [] =>
    6.26 -        (Options.set_default options;
    6.27 -         use_theories last_timing options (map (rpair Position.none) thys))
    6.28 +        Thy_Info.use_thys_options last_timing master_dir options
    6.29 +          (map (rpair Position.none) thys)
    6.30      | conds =>
    6.31          Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    6.32            " (undefined " ^ commas conds ^ ")\n"))
    6.33    end;
    6.34  
    6.35 -in
    6.36 -
    6.37  fun build args_file = Command_Line.tool0 (fn () =>
    6.38      let
    6.39        val _ = SHA1_Samples.test ();
    6.40 @@ -156,7 +140,7 @@
    6.41  
    6.42        val res1 =
    6.43          theories |>
    6.44 -          (List.app (use_theories_condition last_timing)
    6.45 +          (List.app (use_theories last_timing Path.current)
    6.46              |> session_timing name verbose
    6.47              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    6.48              |> Multithreading.max_threads_setmp (Options.int options "threads")
    6.49 @@ -169,5 +153,3 @@
    6.50      in () end);
    6.51  
    6.52  end;
    6.53 -
    6.54 -end;
     7.1 --- a/src/Pure/build-jars	Sun Jan 11 21:06:47 2015 +0100
     7.2 +++ b/src/Pure/build-jars	Tue Jan 13 21:46:09 2015 +0100
     7.3 @@ -55,6 +55,7 @@
     7.4    Isar/parse.scala
     7.5    Isar/token.scala
     7.6    ML/ml_lex.scala
     7.7 +  PIDE/batch_session.scala
     7.8    PIDE/command.scala
     7.9    PIDE/command_span.scala
    7.10    PIDE/document.scala