Impressum protocol_command.ML Sprache: SML

(*  Title:      Pure/PIDE/protocol_command.ML
    Author:     Makarius

Protocol commands.
*)

signature PROTOCOL_COMMAND =
sig
  exception STOP of int
  val is_protocol_exn: exn -> bool
  val define_bytes: string -> (Bytes.T list -> unit) -> unit
  val define: string -> (string list -> unit) -> unit
  val run: string -> Bytes.T list -> unit
end;

structure Protocol_Command: PROTOCOL_COMMAND =
struct

exception STOP of int;

val is_protocol_exn = fn STOP _ => true | _ => false;

local

val commands =
  Synchronized.var "Protocol_Command.commands"
    (Symtab.empty: (Bytes.T list -> unit) Symtab.table);

in

fun define_bytes name cmd =
  Synchronized.change commands (fn cmds =>
   (if not (Symtab.defined cmds name) then ()
    else warning ("Redefining Isabelle protocol command " ^ quote name);
    Symtab.update (name, cmd) cmds));

fun define name cmd = define_bytes name (map Bytes.content #> cmd);

fun run name args =
  (case Symtab.lookup (Synchronized.value commands) name of
    NONE => error ("Undefined Isabelle protocol command " ^ quote name)
  | SOME cmd =>
      (case Exn.capture_body (fn () => Runtime.exn_trace_system (fn () => cmd args)) of
        Exn.Res res => res
      | Exn.Exn exn =>
          if is_protocol_exn exn then Exn.reraise exn
          else error ("Isabelle protocol command failure: " ^ quote name)));

end;

end;

quality100%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.