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


products/sources/formale Sprachen/Isabelle/Pure/General/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 1 kB

Quelle print_mode.ML Sprache: SML

(*  Title:      Pure/General/print_mode.ML
    Author:     Makarius

Generic print mode as thread-local value derived from global template;
provides implicit configuration for various output mechanisms.

The special print mode "input" is never enabled for output.
*)

signature BASIC_PRINT_MODE =
sig
  val print_mode: string list Unsynchronized.ref  (*global template*)
  val print_mode_value: unit -> string list       (*thread-local value*)
  val print_mode_active: string -> bool           (*thread-local value*)
end;

signature PRINT_MODE =
sig
  include BASIC_PRINT_MODE
  val input: string
  val internal: string
  val ASCII: string
  val PIDE: string
  val latex: string
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
  val add_modes: string list -> unit
  val PIDE_enabled: unit -> bool
end;

structure Print_Mode: PRINT_MODE =
struct

val input = "input";
val internal = "internal";
val ASCII = "ASCII";
val PIDE = "PIDE";
val latex = "latex";

val print_mode = Unsynchronized.ref ([]: string list);
val print_mode_var = Thread_Data.var () : string list Thread_Data.var;

fun print_mode_value () =
  let val modes =
    (case Thread_Data.get print_mode_var of
      SOME modes => modes
    | NONE => ! print_mode)
  in subtract (op =) [input, internal] modes end;

fun print_mode_active mode = member (op =) (print_mode_value ()) mode;

fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;

fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;

fun add_modes modes = Unsynchronized.change print_mode (append modes);

fun PIDE_enabled () =
  find_first (fn mode => mode = PIDE orelse mode = "") (print_mode_value ()) = SOME PIDE;

end;

structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
open Basic_Print_Mode;

quality98%

¤ Dauer der Verarbeitung: 0.3 Sekunden ¤

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.