clarified build_theories;
authorwenzelm
Wed Jan 14 14:28:52 2015 +0100 (2015-01-14)
changeset 593643b5da177ae6b
parent 59363 4660b0409096
child 59365 b5d43b01a6b3
clarified build_theories;
src/Pure/PIDE/batch_session.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.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
     1.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Jan 14 11:52:08 2015 +0100
     1.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Jan 14 14:28:52 2015 +0100
     1.3 @@ -44,11 +44,11 @@
     1.4      prover_session.phase_changed +=
     1.5        Session.Consumer[Session.Phase](getClass.getName) {
     1.6          case Session.Ready =>
     1.7 +          val id = Document_ID.make().toString
     1.8            val master_dir = session_info.dir
     1.9 -          for ((_, thy_options, thy_files) <- session_info.theories) {
    1.10 -            val id = Document_ID.make().toString
    1.11 -            prover_session.use_theories(options, id, master_dir, thy_files) // FIXME proper check of result!?
    1.12 -          }
    1.13 +          val theories = session_info.theories.map({ case (_, opts, thys) => (opts, thys) })
    1.14 +          prover_session.build_theories(id, master_dir, theories)
    1.15 +          // FIXME proper check of result!?
    1.16          case Session.Inactive | Session.Failed =>
    1.17            result.fulfill_result(Exn.Exn(ERROR("Prover process terminated")))
    1.18          case Session.Shutdown =>
     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Jan 14 11:52:08 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Jan 14 14:28:52 2015 +0100
     2.3 @@ -186,7 +186,7 @@
     2.4    val command_timing: Properties.entry
     2.5    val loading_theory: string -> Properties.T
     2.6    val dest_loading_theory: Properties.T -> string option
     2.7 -  val use_theories_result: string -> bool -> Properties.T
     2.8 +  val build_theories_result: string -> bool -> Properties.T
     2.9    val print_operationsN: string
    2.10    val print_operations: Properties.T
    2.11    val simp_trace_panelN: string
    2.12 @@ -597,8 +597,8 @@
    2.13  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
    2.14    | dest_loading_theory _ = NONE;
    2.15  
    2.16 -fun use_theories_result id ok =
    2.17 -  [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
    2.18 +fun build_theories_result id ok =
    2.19 +  [("function", "build_theories_result"), ("id", id), ("ok", print_bool ok)];
    2.20  
    2.21  val print_operationsN = "print_operations";
    2.22  val print_operations = [(functionN, print_operationsN)];
     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Jan 14 11:52:08 2015 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Jan 14 14:28:52 2015 +0100
     3.3 @@ -467,11 +467,11 @@
     3.4        }
     3.5    }
     3.6  
     3.7 -  object Use_Theories_Result
     3.8 +  object Build_Theories_Result
     3.9    {
    3.10      def unapply(props: Properties.T): Option[(String, Boolean)] =
    3.11        props match {
    3.12 -        case List((FUNCTION, "use_theories_result"),
    3.13 +        case List((FUNCTION, "build_theories_result"),
    3.14            ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    3.15          case _ => None
    3.16        }
     4.1 --- a/src/Pure/PIDE/protocol.ML	Wed Jan 14 11:52:08 2015 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Wed Jan 14 14:28:52 2015 +0100
     4.3 @@ -111,19 +111,21 @@
     4.4          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
     4.5  
     4.6  val _ =
     4.7 -  Isabelle_Process.protocol_command "use_theories"
     4.8 -    (fn options_yxml :: id :: master_dir :: thys =>
     4.9 +  Isabelle_Process.protocol_command "build_theories"
    4.10 +    (fn [id, master_dir, theories_yxml] =>
    4.11        let
    4.12 -        val options = Options.decode (YXML.parse_body options_yxml);
    4.13 +        val theories =
    4.14 +          YXML.parse_body theories_yxml |>
    4.15 +            let open XML.Decode
    4.16 +            in list (pair Options.decode (list (string #> rpair Position.none))) end;
    4.17          val result =
    4.18            Exn.capture (fn () =>
    4.19 -            Thy_Info.use_thys_options (K NONE) (Path.explode master_dir) options
    4.20 -              (map (rpair Position.none) thys)) ();
    4.21 +            theories |> List.app (Thy_Info.build_theories (K NONE) (Path.explode master_dir))) ();
    4.22          val ok =
    4.23            (case result of
    4.24              Exn.Res _ => true
    4.25            | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    4.26 -    in Output.protocol_message (Markup.use_theories_result id ok) [] end);
    4.27 +    in Output.protocol_message (Markup.build_theories_result id ok) [] end);
    4.28  
    4.29  val _ =
    4.30    Isabelle_Process.protocol_command "ML_System.share_common_data"
     5.1 --- a/src/Pure/PIDE/protocol.scala	Wed Jan 14 11:52:08 2015 +0100
     5.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Jan 14 14:28:52 2015 +0100
     5.3 @@ -456,8 +456,8 @@
     5.4    def remove_versions(versions: List[Document.Version])
     5.5    {
     5.6      val versions_yxml =
     5.7 -      { import XML.Encode._
     5.8 -        YXML.string_of_body(list(long)(versions.map(_.id))) }
     5.9 +    { import XML.Encode._
    5.10 +      YXML.string_of_body(list(long)(versions.map(_.id))) }
    5.11      protocol_command("Document.remove_versions", versions_yxml)
    5.12    }
    5.13  
    5.14 @@ -468,10 +468,13 @@
    5.15      protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
    5.16  
    5.17  
    5.18 -  /* use_theories */
    5.19 +  /* build_theories */
    5.20  
    5.21 -  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path]): Unit =
    5.22 -    protocol_command("use_theories",
    5.23 -      (YXML.string_of_body(Options.encode(options)) ::
    5.24 -        id :: master_dir.implode :: thys.map(_.implode)): _*)
    5.25 +  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
    5.26 +  {
    5.27 +    val theories_yxml =
    5.28 +    { import XML.Encode._
    5.29 +      YXML.string_of_body(list(pair(Options.encode, list(Path.encode)))(theories)) }
    5.30 +    protocol_command("build_theories", id, master_dir.implode, theories_yxml)
    5.31 +  }
    5.32  }
     6.1 --- a/src/Pure/PIDE/session.scala	Wed Jan 14 11:52:08 2015 +0100
     6.2 +++ b/src/Pure/PIDE/session.scala	Wed Jan 14 14:28:52 2015 +0100
     6.3 @@ -63,7 +63,7 @@
     6.4    case object Caret_Focus
     6.5    case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
     6.6    case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
     6.7 -  case class Use_Theories(options: Options, id: String, master_dir: Path, thys: List[Path])
     6.8 +  case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
     6.9    case class Commands_Changed(
    6.10      assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    6.11  
    6.12 @@ -554,8 +554,8 @@
    6.13              prover.get.dialog_result(serial, result)
    6.14              handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result)))
    6.15  
    6.16 -          case Session.Use_Theories(options, id, master_dir, thys) if prover.defined =>
    6.17 -            prover.get.use_theories(options, id, master_dir, thys)
    6.18 +          case Session.Build_Theories(id, master_dir, theories) if prover.defined =>
    6.19 +            prover.get.build_theories(id, master_dir, theories)
    6.20  
    6.21            case Protocol_Command(name, args) if prover.defined =>
    6.22              prover.get.protocol_command(name, args:_*)
    6.23 @@ -620,6 +620,6 @@
    6.24    def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
    6.25    { manager.send(Session.Dialog_Result(id, serial, result)) }
    6.26  
    6.27 -  def use_theories(options: Options, id: String, master_dir: Path, thys: List[Path])
    6.28 -  { manager.send(Session.Use_Theories(options, id, master_dir, thys)) }
    6.29 +  def build_theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
    6.30 +  { manager.send(Session.Build_Theories(id, master_dir, theories)) }
    6.31  }
     7.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jan 14 11:52:08 2015 +0100
     7.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jan 14 14:28:52 2015 +0100
     7.3 @@ -14,8 +14,8 @@
     7.4    val remove_thy: string -> unit
     7.5    val use_thys: (string * Position.T) list -> unit
     7.6    val use_thy: string * Position.T -> unit
     7.7 -  val use_thys_options: (Toplevel.transition -> Time.time option) -> Path.T ->
     7.8 -    Options.T -> (string * Position.T) list -> unit
     7.9 +  val build_theories: (Toplevel.transition -> Time.time option) -> Path.T ->
    7.10 +    Options.T * (string * Position.T) list -> unit
    7.11    val script_thy: Position.T -> string -> theory -> theory
    7.12    val register_thy: theory -> unit
    7.13    val finish: unit -> unit
    7.14 @@ -342,18 +342,30 @@
    7.15  val use_thys = use_theories {document = false, last_timing = K NONE, master_dir = Path.current};
    7.16  val use_thy = use_thys o single;
    7.17  
    7.18 -fun use_thys_options last_timing master_dir options thys =
    7.19 -  (Options.set_default options;
    7.20 -    (use_theories {
    7.21 -        document = Present.document_enabled (Options.string options "document"),
    7.22 -        last_timing = last_timing,
    7.23 -        master_dir = master_dir}
    7.24 -      |> Unsynchronized.setmp print_mode
    7.25 -          (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    7.26 -      |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    7.27 -      |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    7.28 -      |> Multithreading.max_threads_setmp (Options.int options "threads")
    7.29 -      |> Unsynchronized.setmp Future.ML_statistics true) thys);
    7.30 +
    7.31 +(* theories in batch build *)
    7.32 +
    7.33 +fun build_theories last_timing master_dir (options, thys) =
    7.34 +  let
    7.35 +    val condition = space_explode "," (Options.string options "condition");
    7.36 +    val conds = filter_out (can getenv_strict) condition;
    7.37 +  in
    7.38 +    if null conds then
    7.39 +      (Options.set_default options;
    7.40 +        (use_theories {
    7.41 +          document = Present.document_enabled (Options.string options "document"),
    7.42 +          last_timing = last_timing,
    7.43 +          master_dir = master_dir}
    7.44 +        |> Unsynchronized.setmp print_mode
    7.45 +            (space_explode "," (Options.string options "print_mode") @ print_mode_value ())
    7.46 +        |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs")
    7.47 +        |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace")
    7.48 +        |> Multithreading.max_threads_setmp (Options.int options "threads")
    7.49 +        |> Unsynchronized.setmp Future.ML_statistics true) thys)
    7.50 +    else
    7.51 +      Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^
    7.52 +        " (undefined " ^ commas conds ^ ")\n")
    7.53 +  end;
    7.54  
    7.55  
    7.56  (* toplevel scripting -- without maintaining database *)
     8.1 --- a/src/Pure/Tools/build.ML	Wed Jan 14 11:52:08 2015 +0100
     8.2 +++ b/src/Pure/Tools/build.ML	Wed Jan 14 14:28:52 2015 +0100
     8.3 @@ -97,17 +97,6 @@
     8.4  
     8.5  (* build *)
     8.6  
     8.7 -fun use_theories last_timing master_dir (options, thys) =
     8.8 -  let val condition = space_explode "," (Options.string options "condition") in
     8.9 -    (case filter_out (can getenv_strict) condition of
    8.10 -      [] =>
    8.11 -        Thy_Info.use_thys_options last_timing master_dir options
    8.12 -          (map (rpair Position.none) thys)
    8.13 -    | conds =>
    8.14 -        Output.physical_stderr ("Skipping theories " ^ commas_quote thys ^
    8.15 -          " (undefined " ^ commas conds ^ ")\n"))
    8.16 -  end;
    8.17 -
    8.18  fun build args_file = Command_Line.tool0 (fn () =>
    8.19      let
    8.20        val _ = SHA1_Samples.test ();
    8.21 @@ -118,7 +107,7 @@
    8.22            let open XML.Decode in
    8.23              pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    8.24                (pair (list (pair string string)) (pair string (pair string (pair string
    8.25 -                ((list (pair Options.decode (list string))))))))))))
    8.26 +                ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))
    8.27            end;
    8.28  
    8.29        val _ = Options.set_default options;
    8.30 @@ -140,7 +129,7 @@
    8.31  
    8.32        val res1 =
    8.33          theories |>
    8.34 -          (List.app (use_theories last_timing Path.current)
    8.35 +          (List.app (Thy_Info.build_theories last_timing Path.current)
    8.36              |> session_timing name verbose
    8.37              |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    8.38              |> Multithreading.max_threads_setmp (Options.int options "threads")