Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: pure_syn.ML Sprache: SML

Original von: Isabelle^©

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

Outer syntax for bootstrapping: commands that are accessible outside a
regular theory context.
*)

signature PURE_SYN =
sig
  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
    Toplevel.transition -> Toplevel.transition
  val bootstrap_thy: theory
end;

structure Pure_Syn: PURE_SYN =
struct

val semi = Scan.option (Parse.$$$ ";");

fun output_document state markdown txt =
  let
    val ctxt = Toplevel.presentation_context state;
    val pos = Input.pos_of txt;
    val _ =
      Context_Position.reports ctxt
        [(pos, Markup.language_document (Input.is_delimited txt)),
         (pos, Markup.plain_text)];
  in Thy_Output.output_document ctxt markdown txt end;

fun document_command markdown (loc, txt) =
  Toplevel.keep (fn state =>
    (case loc of
      NONE => ignore (output_document state markdown txt)
    | SOME (_, pos) =>
        error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
  Toplevel.present_local_theory loc (fn state =>
    ignore (output_document state markdown txt));

val _ =
  Outer_Syntax.command ("chapter", \<^here>) "chapter heading"
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});

val _ =
  Outer_Syntax.command ("section", \<^here>) "section heading"
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});

val _ =
  Outer_Syntax.command ("subsection", \<^here>) "subsection heading"
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});

val _ =
  Outer_Syntax.command ("subsubsection", \<^here>) "subsubsection heading"
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});

val _ =
  Outer_Syntax.command ("paragraph", \<^here>) "paragraph heading"
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});

val _ =
  Outer_Syntax.command ("subparagraph", \<^here>) "subparagraph heading"
    (Parse.opt_target -- Parse.document_source --| semi >> document_command {markdown = false});

val _ =
  Outer_Syntax.command ("text", \<^here>) "formal comment (primary style)"
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});

val _ =
  Outer_Syntax.command ("txt", \<^here>) "formal comment (secondary style)"
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});

val _ =
  Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
    (Parse.opt_target -- Parse.document_source >> document_command {markdown = true});

val _ =
  Outer_Syntax.command ("theory", \<^here>) "begin theory"
    (Thy_Header.args >>
      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));

val bootstrap_thy = Context.the_global_context ();

val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);

end;

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