diff --git a/src/Doc/Isar_Ref/Symbols.thy b/src/Doc/Isar_Ref/Symbols.thy --- a/src/Doc/Isar_Ref/Symbols.thy +++ b/src/Doc/Isar_Ref/Symbols.thy @@ -1,40 +1,40 @@ (*:maxLineLen=78:*) theory Symbols imports Main Base begin chapter \Predefined Isabelle symbols \label{app:symbols}\ text \ Isabelle supports an infinite number of non-ASCII symbols, which are represented in source text as \<^verbatim>\\\\<^verbatim>\<\\name\\<^verbatim>\>\ (where \name\ may be any identifier). It is left to front-end tools how to present these symbols to the user. The collection of predefined standard symbols given below is available by default for Isabelle document output, due to appropriate definitions of \<^verbatim>\\isasym\\name\ for each \<^verbatim>\\\\<^verbatim>\<\\name\\<^verbatim>\>\ in the \<^verbatim>\isabellesym.sty\ file. Most of these symbols are displayed properly in Isabelle/jEdit and {\LaTeX} generated from Isabelle. Moreover, any single symbol (or ASCII character) may be prefixed by \<^verbatim>\\<^sup>\ for superscript and \<^verbatim>\\<^sub>\ for subscript, such as \<^verbatim>\A\<^sup>\\ for \A\<^sup>\\ and \<^verbatim>\A\<^sub>1\ for \A\<^sub>1\. Sub- and superscripts that span a region of text can be marked up with \<^verbatim>\\<^bsub>\\\\\<^verbatim>\\<^esub>\ and \<^verbatim>\\<^bsup>\\\\\<^verbatim>\\<^esup>\ respectively, but note that there are limitations in the typographic rendering quality of this form. Furthermore, all ASCII characters and most other symbols may be printed in bold by prefixing \<^verbatim>\\<^bold>\ such as \<^verbatim>\\<^bold>\\ for \\<^bold>\\. Note that \<^verbatim>\\<^sup>\, \<^verbatim>\\<^sub>\, \<^verbatim>\\<^bold>\ cannot be combined. Further details of Isabelle document preparation are covered in \chref{ch:document-prep}. \begin{center} \begin{isabellebody} - \input{syms} + @{show_symbols} \end{isabellebody} \end{center} \ end diff --git a/src/Doc/Isar_Ref/document/build b/src/Doc/Isar_Ref/document/build --- a/src/Doc/Isar_Ref/document/build +++ b/src/Doc/Isar_Ref/document/build @@ -1,10 +1,8 @@ #!/usr/bin/env bash set -e FORMAT="$1" VARIANT="$2" -./showsymbols "$ISABELLE_HOME/lib/texinputs/isabellesym.sty" > syms.tex "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" - diff --git a/src/Doc/Isar_Ref/document/showsymbols b/src/Doc/Isar_Ref/document/showsymbols deleted file mode 100755 --- a/src/Doc/Isar_Ref/document/showsymbols +++ /dev/null @@ -1,23 +0,0 @@ -#!/usr/bin/env perl - -print "\\begin{supertabular}{ll\@{\\qquad}ll}\n"; - -$eol = "&"; - -while () { - if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) { - print "\\verb,\\<$1>, & {\\isasym$1} $eol\n"; - if ("$eol" eq "&") { - $eol = "\\\\"; - } else { - $eol = "&"; - } - } -} - -if ("$eol" eq "\\\\") { - print "$eol\n"; -} - -print "\\end{supertabular}\n"; - diff --git a/src/Doc/ROOT b/src/Doc/ROOT --- a/src/Doc/ROOT +++ b/src/Doc/ROOT @@ -1,526 +1,525 @@ chapter Doc session Classes (doc) in "Classes" = HOL + options [document_logo = "Isar", document_build = "build", document_variants = "classes", quick_and_dirty] theories [document = false] Setup theories Classes document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Codegen (doc) in "Codegen" = HOL + options [document_logo = "Isar", document_build = "build", document_variants = "codegen", print_mode = "no_brackets,iff"] sessions "HOL-Library" theories [document = false] Setup theories Introduction Foundations Refinement Inductive_Predicate Evaluation Computations Adaptation Further document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Corec (doc) in "Corec" = Datatypes + options [document_build = "build", document_variants = "corec"] theories Corec document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Datatypes (doc) in "Datatypes" = HOL + options [document_build = "build", document_variants = "datatypes"] sessions "HOL-Library" theories [document = false] Setup theories Datatypes document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Eisbach (doc) in "Eisbach" = HOL + options [document_logo = "Eisbach", document_build = "build", document_variants = "eisbach", quick_and_dirty, print_mode = "no_brackets,iff", show_question_marks = false] sessions "HOL-Eisbach" theories [document = false] Base theories Preface Manual document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Functions (doc) in "Functions" = HOL + options [document_build = "build", document_variants = "functions", skip_proofs = false, quick_and_dirty] theories Functions document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "conclusion.tex" "intro.tex" "root.tex" "style.sty" session How_to_Prove_it (no_doc) in "How_to_Prove_it" = HOL + options [document_variants = "how_to_prove_it", show_question_marks = false] theories How_to_Prove_it document_files "root.tex" "root.bib" "prelude.tex" session Intro (doc) in "Intro" = Pure + options [document_logo = "_", document_build = "build", document_variants = "intro"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "ttbox.sty" "manual.bib" document_files "advanced.tex" "build" "foundations.tex" "getting.tex" "root.tex" session Implementation (doc) in "Implementation" = HOL + options [document_logo = "Isar", document_build = "build", document_variants = "implementation", quick_and_dirty] theories Eq Integration Isar Local_Theory "ML" Prelim Proof Syntax Tactic theories [parallel_proofs = 0] Logic document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files "build" "root.tex" "style.sty" session Isar_Ref (doc) in "Isar_Ref" = HOL + options [document_logo = "Isar", document_build = "build", document_variants = "isar-ref", quick_and_dirty, thy_output_source] sessions "HOL-Library" theories Preface Synopsis Framework First_Order_Logic Outer_Syntax Document_Preparation Spec Proof Proof_Script Inner_Syntax Generic HOL_Specific Quick_Reference Symbols document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files "build" "isar-vm.pdf" "isar-vm.svg" "root.tex" - "showsymbols" "style.sty" session JEdit (doc) in "JEdit" = HOL + options [document_logo = "jEdit", document_build = "build", document_variants = "jedit", thy_output_source] theories JEdit document_files (in "..") "extra.sty" "iman.sty" "isar.sty" "manual.bib" "pdfsetup.sty" "prepare_document" "ttbox.sty" "underscore.sty" document_files (in "../Isar_Ref/document") "style.sty" document_files "auto-tools.png" "bibtex-mode.png" "build" "cite-completion.png" "isabelle-jedit.png" "markdown-document.png" "ml-debugger.png" "output-and-state.png" "output-including-state.png" "output.png" "popup1.png" "popup2.png" "query.png" "root.tex" "scope1.png" "scope2.png" "sidekick-document.png" "sidekick.png" "sledgehammer.png" "theories.png" session Sugar (doc) in "Sugar" = HOL + options [document_build = "build", document_variants = "sugar"] sessions "HOL-Library" theories Sugar document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "build" "root.bib" "root.tex" session Locales (doc) in "Locales" = HOL + options [document_build = "build", document_variants = "locales", thy_output_margin = 65, skip_proofs = false] theories Examples1 Examples2 Examples3 document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "build" "root.bib" "root.tex" session Logics (doc) in "Logics" = Pure + options [document_logo = "_", document_build = "build", document_variants = "logics"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "ttbox.sty" "manual.bib" document_files "CTT.tex" "HOL.tex" "LK.tex" "Sequents.tex" "build" "preface.tex" "root.tex" "syntax.tex" session Logics_ZF (doc) in "Logics_ZF" = ZF + options [document_logo = "ZF", document_build = "build", document_variants = "logics-ZF", print_mode = "brackets", thy_output_source] sessions FOL theories IFOL_examples FOL_examples ZF_examples If ZF_Isar document_files (in "..") "prepare_document" "pdfsetup.sty" "isar.sty" "ttbox.sty" "manual.bib" document_files (in "../Logics/document") "syntax.tex" document_files "FOL.tex" "ZF.tex" "build" "logics.sty" "root.tex" session Main (doc) in "Main" = HOL + options [document_build = "build", document_variants = "main"] theories Main_Doc document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "build" "root.tex" session Nitpick (doc) in "Nitpick" = Pure + options [document_logo = "Nitpick", document_build = "build", document_variants = "nitpick"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "manual.bib" document_files "build" "root.tex" session Prog_Prove (doc) in "Prog_Prove" = HOL + options [document_logo = "HOL", document_build = "build", document_variants = "prog-prove", show_question_marks = false] theories Basics Bool_nat_list MyList Types_and_funs Logic Isar document_files (in ".") "MyList.thy" document_files (in "..") "prepare_document" "pdfsetup.sty" document_files "bang.pdf" "build" "intro-isabelle.tex" "prelude.tex" "root.bib" "root.tex" "svmono.cls" session Sledgehammer (doc) in "Sledgehammer" = Pure + options [document_logo = "S/H", document_build = "build", document_variants = "sledgehammer"] document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "manual.bib" document_files "build" "root.tex" session System (doc) in "System" = Pure + options [document_logo = "_", document_build = "build", document_variants = "system", thy_output_source] sessions "HOL-Library" theories Environment Sessions Presentation Server Scala Phabricator Misc document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "ttbox.sty" "underscore.sty" "manual.bib" document_files (in "../Isar_Ref/document") "style.sty" document_files "build" "root.tex" session Tutorial (doc) in "Tutorial" = HOL + options [document_logo = "HOL", document_build = "build", document_variants = "tutorial", print_mode = "brackets", skip_proofs = false] directories "Advanced" "CTL" "CodeGen" "Datatype" "Documents" "Fun" "Ifexpr" "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types" theories [document = false] Base theories [threads = 1] "ToyList/ToyList_Test" theories [thy_output_indent = 5] "ToyList/ToyList" "Ifexpr/Ifexpr" "CodeGen/CodeGen" "Trie/Trie" "Datatype/ABexpr" "Datatype/unfoldnested" "Datatype/Nested" "Datatype/Fundata" "Fun/fun0" "Advanced/simp2" "CTL/PDL" "CTL/CTL" "CTL/CTLind" "Inductive/Even" "Inductive/Mutual" "Inductive/Star" "Inductive/AB" "Inductive/Advanced" "Misc/Tree" "Misc/Tree2" "Misc/Plus" "Misc/case_exprs" "Misc/fakenat" "Misc/natsum" "Misc/pairs2" "Misc/Option2" "Misc/types" "Misc/prime_def" "Misc/simp" "Misc/Itrev" "Misc/AdvancedInd" "Misc/appendix" theories "Protocol/NS_Public" "Documents/Documents" theories [thy_output_margin = 64, thy_output_indent = 0] "Types/Numbers" "Types/Pairs" "Types/Records" "Types/Typedefs" "Types/Overloading" "Types/Axioms" "Rules/Basic" "Rules/Blast" "Rules/Force" theories [thy_output_margin = 64, thy_output_indent = 5] "Rules/TPrimes" "Rules/Forward" "Rules/Tacticals" "Rules/find2" "Sets/Examples" "Sets/Functions" "Sets/Relations" "Sets/Recur" document_files (in "ToyList") "ToyList1.txt" "ToyList2.txt" document_files (in "..") "pdfsetup.sty" "ttbox.sty" "manual.bib" document_files "advanced0.tex" "appendix0.tex" "basics.tex" "build" "cl2emono-modified.sty" "ctl0.tex" "documents0.tex" "fp.tex" "inductive0.tex" "isa-index" "Isa-logics.pdf" "numerics.tex" "pghead.pdf" "preface.tex" "protocol.tex" "root.tex" "rules.tex" "sets.tex" "tutorial.sty" "typedef.pdf" "types0.tex" session Typeclass_Hierarchy (doc) in "Typeclass_Hierarchy" = HOL + options [document_logo = "Isar", document_build = "build", document_variants = "typeclass_hierarchy"] sessions "HOL-Library" theories [document = false] Setup theories Typeclass_Hierarchy document_files (in "..") "prepare_document" "pdfsetup.sty" "iman.sty" "extra.sty" "isar.sty" "manual.bib" document_files "build" "root.tex" "style.sty" diff --git a/src/Doc/antiquote_setup.ML b/src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML +++ b/src/Doc/antiquote_setup.ML @@ -1,210 +1,242 @@ (* Title: Doc/antiquote_setup.ML Author: Makarius Auxiliary antiquotations for the Isabelle manuals. *) structure Antiquote_Setup: sig end = struct (* misc utils *) fun translate f = Symbol.explode #> map f #> implode; val clean_string = translate (fn "_" => "\\_" | "#" => "\\#" | "$" => "\\$" | "%" => "\\%" | "<" => "$<$" | ">" => "$>$" | "{" => "\\{" | "|" => "$\\mid$" | "}" => "\\}" | "\" => "-" | c => c); fun clean_name "\" = "dots" | clean_name ".." = "ddot" | clean_name "." = "dot" | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | c => c); (* ML text *) local fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");" | ml_val (toks1, toks2) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");" | ml_op (toks1, toks2) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;" | ml_type (toks1, toks2) = ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @ toks2 @ ML_Lex.read ") option];"; fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);" | ml_exception (toks1, toks2) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);"; fun ml_structure (toks, _) = ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;"; fun ml_functor (Antiquote.Text tok :: _, _) = ML_Lex.read "ML_Env.check_functor " @ ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) | ml_functor _ = raise Fail "Bad ML functor specification"; val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident); fun ml_name txt = (case filter is_name (ML_Lex.tokenize txt) of toks as [_] => ML_Lex.flatten toks | _ => error ("Single ML name expected in input: " ^ quote txt)); fun prep_ml source = (#1 (Input.source_content source), ML_Lex.read_source source); fun index_ml name kind ml = Thy_Output.antiquotation_raw name (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input))) (fn ctxt => fn (source1, opt_source2) => let val (txt1, toks1) = prep_ml source1; val (txt2, toks2) = (case opt_source2 of SOME source => prep_ml source | NONE => ("", [])); val txt = if txt2 = "" then txt1 else if kind = "type" then txt1 ^ " = " ^ txt2 else if kind = "exception" then txt1 ^ " of " ^ txt2 else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) then txt1 ^ ": " ^ txt2 else txt1 ^ " : " ^ txt2; val txt' = if kind = "" then txt else kind ^ " " ^ txt; val pos = Input.pos_of source1; val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) handle ERROR msg => error (msg ^ Position.here pos); val kind' = if kind = "" then "ML" else "ML " ^ kind; in Latex.block [Latex.string ("\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}"), Thy_Output.verbatim ctxt txt'] end); in val _ = Theory.setup (index_ml \<^binding>\index_ML\ "" ml_val #> index_ml \<^binding>\index_ML_op\ "infix" ml_op #> index_ml \<^binding>\index_ML_type\ "type" ml_type #> index_ml \<^binding>\index_ML_exception\ "exception" ml_exception #> index_ml \<^binding>\index_ML_structure\ "structure" ml_structure #> index_ml \<^binding>\index_ML_functor\ "functor" ml_functor); end; (* named theorems *) val _ = Theory.setup (Thy_Output.antiquotation_raw \<^binding>\named_thms\ (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) (fn ctxt => map (fn (thm, name) => Output.output (Document_Antiquotation.format ctxt (Document_Antiquotation.delimit ctxt (Thy_Output.pretty_thm ctxt thm))) ^ enclose "\\rulename{" "}" (Output.output name)) #> space_implode "\\par\\smallskip%\n" #> Latex.string #> single #> Thy_Output.isabelle ctxt)); (* Isabelle/Isar entities (with index) *) local fun no_check (_: Proof.context) (name, _: Position.T) = name; fun check_keyword ctxt (name, pos) = if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then name else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos); fun check_system_option ctxt arg = (Completion.check_option (Options.default ()) ctxt arg; true) handle ERROR _ => false; val arg = enclose "{" "}" o clean_string; fun entity check markup binding index = Thy_Output.antiquotation_raw (binding |> Binding.map_name (fn name => name ^ (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name_position)) (fn ctxt => fn (logic, (name, pos)) => let val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); val hyper_name = "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; val hyper = enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; val idx = (case index of NONE => "" | SOME is_def => "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); val _ = if Context_Position.is_reported ctxt pos then ignore (check ctxt (name, pos)) else (); val latex = idx ^ (Output.output name |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |> hyper o enclose "\\mbox{\\isa{" "}}"); in Latex.string latex end); fun entity_antiqs check markup kind = entity check markup kind NONE #> entity check markup kind (SOME true) #> entity check markup kind (SOME false); in val _ = Theory.setup (entity_antiqs no_check "" \<^binding>\syntax\ #> entity_antiqs Outer_Syntax.check_command "isacommand" \<^binding>\command\ #> entity_antiqs check_keyword "isakeyword" \<^binding>\keyword\ #> entity_antiqs check_keyword "isakeyword" \<^binding>\element\ #> entity_antiqs Method.check_name "" \<^binding>\method\ #> entity_antiqs Attrib.check_name "" \<^binding>\attribute\ #> entity_antiqs no_check "" \<^binding>\fact\ #> entity_antiqs no_check "" \<^binding>\variable\ #> entity_antiqs no_check "" \<^binding>\case\ #> entity_antiqs Document_Antiquotation.check "" \<^binding>\antiquotation\ #> entity_antiqs Document_Antiquotation.check_option "" \<^binding>\antiquotation_option\ #> entity_antiqs Document_Marker.check "" \<^binding>\document_marker\ #> entity_antiqs no_check "isasystem" \<^binding>\setting\ #> entity_antiqs check_system_option "isasystem" \<^binding>\system_option\ #> entity_antiqs no_check "" \<^binding>\inference\ #> entity_antiqs no_check "isasystem" \<^binding>\executable\ #> entity_antiqs Isabelle_Tool.check "isatool" \<^binding>\tool\ #> entity_antiqs ML_Context.check_antiquotation "" \<^binding>\ML_antiquotation\ #> entity_antiqs (K JEdit.check_action) "isasystem" \<^binding>\action\); end; + +(* show symbols *) + +val _ = + Theory.setup (Thy_Output.antiquotation_raw \<^binding>\show_symbols\ (Scan.succeed ()) + (fn _ => fn _ => + let + val symbol_name = + unprefix "\\newcommand{\\isasym" + #> raw_explode + #> take_prefix Symbol.is_ascii_letter + #> implode; + + val symbols = + File.read \<^file>\~~/lib/texinputs/isabellesym.sty\ + |> split_lines + |> map_filter (fn line => + (case try symbol_name line of + NONE => NONE + | SOME "" => NONE + | SOME name => SOME ("\\verb,\\" ^ "<" ^ name ^ ">, & {\\isasym" ^ name ^ "}"))); + + val eol = "\\\\\n"; + fun table (a :: b :: rest) = a ^ " & " ^ b ^ eol :: table rest + | table [a] = [a ^ eol] + | table [] = []; + in + Latex.string + ("\\begin{supertabular}{ll@{\\qquad}ll}\n" ^ implode (table symbols) ^ + "\\end{supertabular}\n") + end)) + end;