Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: target_context.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/Isar/target_context.ML
    Author:     Florian Haftmann

Handling of named and nested targets at the Isar toplevel via context begin / end blocks.
*)

signature TARGET_CONTEXT =
sig
  val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T ->
    theory -> local_theory
  val end_named_cmd: local_theory -> Context.generic
  val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
    (local_theory -> Context.generic) * local_theory
  val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
    Context.generic -> local_theory
  val end_nested_cmd: local_theory -> Context.generic
end;

structure Target_Context: TARGET_CONTEXT =
struct

fun prep_includes thy =
  map (Bundle.check (Proof_Context.init_global thy));

fun context_begin_named_cmd raw_includes ("-", _) thy =
      Named_Target.init (prep_includes thy raw_includes) "" thy
  | context_begin_named_cmd raw_includes name thy =
      Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy;

val end_named_cmd = Context.Theory o Local_Theory.exit_global;

fun switch_named_cmd NONE (Context.Theory thy) =
      (end_named_cmd, Named_Target.theory_init thy)
  | switch_named_cmd (SOME name) (Context.Theory thy) =
      (end_named_cmd, context_begin_named_cmd [] name thy)
  | switch_named_cmd NONE (Context.Proof lthy) =
      (Context.Proof o Local_Theory.reset, lthy)
  | switch_named_cmd (SOME name) (Context.Proof lthy) =
      let
        val (reinit, thy) = Named_Target.exit_global_reinitialize lthy
      in
        (Context.Proof o reinit o Local_Theory.exit_global,
          context_begin_named_cmd [] name thy)
      end;

fun includes raw_includes lthy =
  Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;

fun context_begin_nested_cmd raw_includes raw_elems gthy =
  gthy
  |> Context.cases Named_Target.theory_init Local_Theory.assert
  |> includes raw_includes
  |> Expression.read_declaration ([], []) I raw_elems
  |> (#4 o fst)
  |> Local_Theory.begin_nested
  |> snd;

fun end_nested_cmd lthy =
  let
    val lthy' = Local_Theory.end_nested lthy
  in
    if Named_Target.is_theory lthy'
    then Context.Theory (Local_Theory.exit_global lthy')
    else Context.Proof lthy'
  end;

end;

structure Local_Theory : LOCAL_THEORY = struct open Local_Theory; end;

¤ Dauer der Verarbeitung: 0.15 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.