(* 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: theoryend ;structure Pure_Syn: PURE_SYN =struct fun document_heading (name, pos) =" heading" )option (Parse.$$$ ";" ) >>false , markup = fn body => [XML.Elem (Markup.latex_heading name, body)]});fun document_body ((name, pos), description) =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 _ ="text_raw" , \<^here>) "LaTeX text (without surrounding environment)" true , markup = XML.enclose "%\n" "\n" });val _ ="theory" , \<^here>) "begin theory" "Missing theory initialization" )));val bootstrap_thy = Context.the_global_context ();val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false );end ;quality 100%
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
