products/Sources/formale Sprachen/VDM/VDMSL/realmSL/   (Wiener Entwicklungsmethode ©)  Datei vom 13.4.2020 mit Größe 1 kB image not shown  

SSL pure_syn.ML   Interaktion und
PortierbarkeitSML

 
(*  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 bootstrap_thy: theory
end;

structure Pure_Syn: PURE_SYN =
struct

fun document_heading (name, pos) =
  Outer_Syntax.command (name, pos) (name ^ " heading")
    (Parse.opt_target -- Parse.document_source --| Scan.option (Parse.$$$ ";") >>
      Document_Output.document_output
        {markdown = false, markup = fn body => [XML.Elem (Markup.latex_heading name, body)]});

fun document_body ((name, pos), description) =
  Outer_Syntax.command (name, pos) description
    (Parse.opt_target -- Parse.document_source >>
      Document_Output.document_output
        {markdown = true, markup = fn body => [XML.Elem (Markup.latex_body name, body)]});

val _ =
  List.app document_heading
   [("chapter", \<^here>),
    ("section", \<^here>),
    ("subsection", \<^here>),
    ("subsubsection", \<^here>),
    ("paragraph", \<^here>),
    ("subparagraph", \<^here>)];

val _ =
  List.app document_body
   [(("text", \<^here>), "formal comment (primary style)"),
    (("txt", \<^here>), "formal comment (secondary style)")];

val _ =
  Outer_Syntax.command ("text_raw", \<^here>) "LaTeX text (without surrounding environment)"
    (Parse.opt_target -- Parse.document_source >>
      Document_Output.document_output
        {markdown = true, markup = XML.enclose "%\n" "\n"});

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;

100%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.15Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Bot Zugriff




Normalansicht

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.