Quelle document_marker.ML Sprache: SML

(*  Title:      Pure/Thy/document_marker.ML
    Author:     Makarius

Document markers: declarations on the presentation context.
*)

signature DOCUMENT_MARKER =
sig
  type marker = Proof.context -> Proof.context
  val check: Proof.context -> string * Position.T -> string * (Token.src -> marker)
  val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
  val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
  val evaluate: string -> Input.source -> marker
  val command_name: Proof.context -> string
  val legacy_tag: string -> Input.source
end;

structure Document_Marker: DOCUMENT_MARKER =
struct

(* theory data *)

type marker = Proof.context -> Proof.context;

structure Markers = Theory_Data
(
  type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
  val empty : T = Name_Space.empty_table "document_marker";
  val merge = Name_Space.merge_tables;
);

val get_markers = Markers.get o Proof_Context.theory_of;

fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt);

fun setup name scan body thy =
  let
    fun marker src ctxt =
      let val (x, ctxt') = Token.syntax scan src ctxt
      in body x ctxt' end;
  in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;

fun setup0 name scan = setup name (Scan.lift scan);

(* evaluate inner syntax *)

val config_command_name = Config.declare_string ("command_name", \<^here>) (K "");
val command_name = Config.apply config_command_name;

val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;

fun evaluate cmd_name input ctxt =
  let
    val syms = Input.source_explode input
      |> drop_prefix (fn (s, _) => s = Symbol.marker);
    val pos = #1 (Symbol_Pos.range syms);

    val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker));

    val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt);
    val body = Symbol_Pos.cartouche_content syms;
    val markers =
      Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body)
      |> Parse.read_embedded ctxt keywords (Parse.list parse_marker);
  in
    ctxt
    |> Config.put config_command_name cmd_name
    |> fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers
    |> Config.put config_command_name (command_name ctxt)
  end;

(* tag with scope *)

val parse_tag =
  Scan.state :|-- (fn context =>
    let
      val ctxt = Context.proof_of context;
      val scope0 =
        if Keyword.is_theory_goal (Thy_Header.get_keywords' ctxt) (command_name ctxt)
        then Document_Source.Command
        else Document_Source.Proof;
      val tag = Scan.optional Document_Source.tag_scope scope0 -- Document_Source.tag_name >> swap;
    in Scan.lift (Parse.position tag) end);

fun update_tags (tag as (name, _), pos) ctxt =
(Context_Position.report ctxt pos (Markup.document_tag name);
  Document_Source.update_tags tag ctxt);

(* concrete markers *)

fun meta_data markup arg ctxt =
  (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt);

val _ =
  Theory.setup
    (setup (Binding.make ("tag", \<^here>)) parse_tag update_tags #>
     setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
     setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
     setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
     setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
     setup0 (Binding.make ("license", \<^here>)) Parse.embedded (meta_data Markup.meta_license) #>
     setup0 (Binding.make ("description", \<^here>)) Parse.embedded_input
      (fn source => fn ctxt =>
        let
          val (arg, pos) = Input.source_content source;
          val _ = Context_Position.report ctxt pos Markup.words;
        in meta_data Markup.meta_description arg ctxt end));

fun legacy_tag name =
  Input.string (cartouche ("tag (proof) " ^ Symbol_Pos.quote_string_qq name));

end;

quality98%

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.