Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 104 kB

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.13 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.