added protocol command "use_theories", with core functionality of batch build;
authorwenzelm
Thu Apr 17 13:21:36 2014 +0200 (2014-04-17 ago)
changeset 56616abc2da18d08d
parent 56615 47c1dbeec36a
child 56617 c00646996701
added protocol command "use_theories", with core functionality of batch build;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/markup.ML	Thu Apr 17 12:03:15 2014 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Thu Apr 17 13:21:36 2014 +0200
     1.3 @@ -184,6 +184,7 @@
     1.4    val command_timing: Properties.entry
     1.5    val loading_theory: string -> Properties.T
     1.6    val dest_loading_theory: Properties.T -> string option
     1.7 +  val use_theories_result: string -> bool -> Properties.T
     1.8    val simp_trace_logN: string
     1.9    val simp_trace_stepN: string
    1.10    val simp_trace_recurseN: string
    1.11 @@ -580,6 +581,9 @@
    1.12  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
    1.13    | dest_loading_theory _ = NONE;
    1.14  
    1.15 +fun use_theories_result id ok =
    1.16 +  [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
    1.17 +
    1.18  
    1.19  (* simplifier trace *)
    1.20  
     2.1 --- a/src/Pure/PIDE/markup.scala	Thu Apr 17 12:03:15 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Thu Apr 17 13:21:36 2014 +0200
     2.3 @@ -420,6 +420,25 @@
     2.4        }
     2.5    }
     2.6  
     2.7 +  object Loading_Theory
     2.8 +  {
     2.9 +    def unapply(props: Properties.T): Option[String] =
    2.10 +      props match {
    2.11 +        case List((FUNCTION, "loading_theory"), (NAME, name)) => Some(name)
    2.12 +        case _ => None
    2.13 +      }
    2.14 +  }
    2.15 +
    2.16 +  object Use_Theories_Result
    2.17 +  {
    2.18 +    def unapply(props: Properties.T): Option[(String, Boolean)] =
    2.19 +      props match {
    2.20 +        case List((FUNCTION, "use_theories_result"),
    2.21 +          ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
    2.22 +        case _ => None
    2.23 +      }
    2.24 +  }
    2.25 +
    2.26  
    2.27    /* simplifier trace */
    2.28  
     3.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 17 12:03:15 2014 +0200
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Apr 17 13:21:36 2014 +0200
     3.3 @@ -108,5 +108,20 @@
     3.4        Active.dialog_result (Markup.parse_int serial) result
     3.5          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
     3.6  
     3.7 +val _ =
     3.8 +  Isabelle_Process.protocol_command "use_theories"
     3.9 +    (fn id :: master_dir :: thys =>
    3.10 +      let
    3.11 +        val result =
    3.12 +          Exn.capture (fn () =>
    3.13 +            Thy_Info.use_theories
    3.14 +              {document = false, last_timing = K NONE, master_dir = Path.explode master_dir}
    3.15 +              (map (rpair Position.none) thys)) ();
    3.16 +        val ok =
    3.17 +          (case result of
    3.18 +            Exn.Res _ => true
    3.19 +          | Exn.Exn exn => (Runtime.exn_error_message exn; false));
    3.20 +    in Output.protocol_message (Markup.use_theories_result id ok) [] end);
    3.21 +
    3.22  end;
    3.23  
     4.1 --- a/src/Pure/PIDE/protocol.scala	Thu Apr 17 12:03:15 2014 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Apr 17 13:21:36 2014 +0200
     4.3 @@ -428,4 +428,10 @@
     4.4  
     4.5    def dialog_result(serial: Long, result: String): Unit =
     4.6      protocol_command("Document.dialog_result", Properties.Value.Long(serial), result)
     4.7 +
     4.8 +
     4.9 +  /* use_theories */
    4.10 +
    4.11 +  def use_theories(id: String, master_dir: Path, thys: List[Path]): Unit =
    4.12 +    protocol_command("use_theories", (id :: master_dir.implode :: thys.map(_.implode)): _*)
    4.13  }