Quelle ml_file.ML Sprache: SML

(*  Title:      Pure/ML/ml_file.ML
    Author:     Makarius

Commands to load ML files.
*)

signature ML_FILE =
sig
  val command: string -> bool -> bool option -> (theory -> Token.file) ->
    Toplevel.transition -> Toplevel.transition
  val ML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
  val SML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
end;

structure ML_File: ML_FILE =
struct

fun command environment catch_all debug get_file = Toplevel.generic_theory (fn gthy =>
  let
    val file = get_file (Context.theory_of gthy);
    val provide = Resources.provide_file file;
    val source = Token.file_source file;

    val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);

    val flags: ML_Compiler.flags =
      {environment = environment, redirect = true, verbose = true, catch_all = catch_all,
        debug = debug, writeln = writeln, warning = warning};
  in
    gthy
    |> Local_Theory.touch_ml_env
    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    |> Local_Theory.propagate_ml_env
    |> Context.mapping provide (Local_Theory.background_theory provide)
  end);

val ML = command "" false;
val SML = command ML_Env.SML true;

end;

quality100%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.