Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: lkt_US.xml Sprache: SML

Original von: Isabelle^©

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

Context position visibility flag.
*)

signature CONTEXT_POSITION =
sig
  val is_visible_generic: Context.generic -> bool
  val is_visible: Proof.context -> bool
  val is_visible_global: theory -> bool
  val set_visible_generic: bool -> Context.generic -> Context.generic
  val set_visible: bool -> Proof.context -> Proof.context
  val set_visible_global: bool -> theory -> theory
  val is_really_visible: Proof.context -> bool
  val not_really: Proof.context -> Proof.context
  val restore_visible_generic: Context.generic -> Context.generic -> Context.generic
  val restore_visible: Proof.context -> Proof.context -> Proof.context
  val restore_visible_global: theory -> theory -> theory
  val pide_reports: unit -> bool
  val reports_enabled_generic: Context.generic -> bool
  val reports_enabled: Proof.context -> bool
  val reports_enabled_global: theory -> bool
  val is_reported_generic: Context.generic -> Position.T -> bool
  val is_reported: Proof.context -> Position.T -> bool
  val is_reported_global: theory -> Position.T -> bool
  val report_generic: Context.generic -> Position.T -> Markup.T -> unit
  val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
  val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
  val report: Proof.context -> Position.T -> Markup.T -> unit
  val reports_text: Proof.context -> Position.report_text list -> unit
  val reports_generic: Context.generic -> Position.report list -> unit
  val reports: Proof.context -> Position.report list -> unit
  val reports_global: theory -> Position.report list -> unit
end;

structure Context_Position: CONTEXT_POSITION =
struct

(* visible context *)

val really = Config.declare_bool ("really", Position.none) (K true);
val visible = Config.declare_bool ("visible", Position.none) (K true);

val is_visible_generic = Config.apply_generic visible;
val is_visible = Config.apply visible;
val is_visible_global = Config.apply_global visible;

val set_visible_generic = Config.put_generic visible;
val set_visible = Config.put visible;
val set_visible_global = Config.put_global visible;

val is_really = Config.apply really;
fun is_really_visible ctxt = is_really ctxt andalso is_visible ctxt;
val not_really = Config.put really false;

fun restore_visible_generic context =
  Config.restore_generic really context #>
  Config.restore_generic visible context;

val restore_visible = Context.proof_map o restore_visible_generic o Context.Proof;
val restore_visible_global = Context.theory_map o restore_visible_generic o Context.Theory;

(* PIDE reports *)

fun pide_reports () = Options.default_bool "pide_reports";

fun reports_enabled_generic context = pide_reports () andalso is_visible_generic context;
val reports_enabled = reports_enabled_generic o Context.Proof;
val reports_enabled_global = reports_enabled_generic o Context.Theory;

fun is_reported_generic context pos =
  reports_enabled_generic context andalso Position.is_reported pos;

val is_reported = is_reported_generic o Context.Proof;
val is_reported_global = is_reported_generic o Context.Theory;

fun report_generic context pos markup =
  if is_reported_generic context pos then
    Output.report [Position.reported_text pos markup ""]
  else ();

fun reported_text ctxt pos markup txt =
  if is_reported ctxt pos then Position.reported_text pos markup txt else "";

fun report_text ctxt pos markup txt = Output.report [reported_text ctxt pos markup txt];
fun report ctxt pos markup = report_text ctxt pos markup "";

fun reports_text ctxt reps =
  if reports_enabled ctxt then Position.reports_text reps else ();

fun reports_generic context reps =
  if reports_enabled_generic context then Position.reports reps else ();

val reports = reports_generic o Context.Proof;
val reports_global = reports_generic o Context.Theory;

end;

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.