diff --git a/etc/symbols b/etc/symbols --- a/etc/symbols +++ b/etc/symbols @@ -1,436 +1,438 @@ # Default interpretation of some Isabelle symbols \ code: 0x01d7ec group: digit \ code: 0x01d7ed group: digit \ code: 0x01d7ee group: digit \ code: 0x01d7ef group: digit \ code: 0x01d7f0 group: digit \ code: 0x01d7f1 group: digit \ code: 0x01d7f2 group: digit \ code: 0x01d7f3 group: digit \ code: 0x01d7f4 group: digit \ code: 0x01d7f5 group: digit \ code: 0x01d49c group: letter \ code: 0x00212c group: letter \ code: 0x01d49e group: letter \ code: 0x01d49f group: letter \ code: 0x002130 group: letter \ code: 0x002131 group: letter \ code: 0x01d4a2 group: letter \ code: 0x00210b group: letter \ code: 0x002110 group: letter \ code: 0x01d4a5 group: letter \ code: 0x01d4a6 group: letter \ code: 0x002112 group: letter \ code: 0x002133 group: letter \ code: 0x01d4a9 group: letter \ code: 0x01d4aa group: letter \

code: 0x01d5c9 group: letter \ code: 0x01d5ca group: letter \ code: 0x01d5cb group: letter \ code: 0x01d5cc group: letter \ code: 0x01d5cd group: letter \ code: 0x01d5ce group: letter \ code: 0x01d5cf group: letter \ code: 0x01d5d0 group: letter \ code: 0x01d5d1 group: letter \ code: 0x01d5d2 group: letter \ code: 0x01d5d3 group: letter \ code: 0x01d504 group: letter \ code: 0x01d505 group: letter \ code: 0x00212d group: letter \

code: 0x01d507 group: letter \ code: 0x01d508 group: letter \ code: 0x01d509 group: letter \ code: 0x01d50a group: letter \ code: 0x00210c group: letter \ code: 0x002111 group: letter \ code: 0x01d50d group: letter \ code: 0x01d50e group: letter \ code: 0x01d50f group: letter \ code: 0x01d510 group: letter \ code: 0x01d511 group: letter \ code: 0x01d512 group: letter \ code: 0x01d513 group: letter \ code: 0x01d514 group: letter \ code: 0x00211c group: letter \ code: 0x01d516 group: letter \ code: 0x01d517 group: letter \ code: 0x01d518 group: letter \ code: 0x01d519 group: letter \ code: 0x01d51a group: letter \ code: 0x01d51b group: letter \ code: 0x01d51c group: letter \ code: 0x002128 group: letter \ code: 0x01d51e group: letter \ code: 0x01d51f group: letter \ code: 0x01d520 group: letter \
code: 0x01d521 group: letter \ code: 0x01d522 group: letter \ code: 0x01d523 group: letter \ code: 0x01d524 group: letter \ code: 0x01d525 group: letter \ code: 0x01d526 group: letter \ code: 0x01d527 group: letter \ code: 0x01d528 group: letter \ code: 0x01d529 group: letter \ code: 0x01d52a group: letter \ code: 0x01d52b group: letter \ code: 0x01d52c group: letter \ code: 0x01d52d group: letter \ code: 0x01d52e group: letter \ code: 0x01d52f group: letter \ code: 0x01d530 group: letter \ code: 0x01d531 group: letter \ code: 0x01d532 group: letter \ code: 0x01d533 group: letter \ code: 0x01d534 group: letter \ code: 0x01d535 group: letter \ code: 0x01d536 group: letter \ code: 0x01d537 group: letter \ code: 0x0003b1 group: greek \ code: 0x0003b2 group: greek \ code: 0x0003b3 group: greek \ code: 0x0003b4 group: greek \ code: 0x0003b5 group: greek \ code: 0x0003b6 group: greek \ code: 0x0003b7 group: greek \ code: 0x0003b8 group: greek \ code: 0x0003b9 group: greek \ code: 0x0003ba group: greek \ code: 0x0003bb group: greek abbrev: % \ code: 0x0003bc group: greek \ code: 0x0003bd group: greek \ code: 0x0003be group: greek \ code: 0x0003c0 group: greek \ code: 0x0003c1 group: greek \ code: 0x0003c3 group: greek \ code: 0x0003c4 group: greek \ code: 0x0003c5 group: greek \ code: 0x0003c6 group: greek \ code: 0x0003c7 group: greek \ code: 0x0003c8 group: greek \ code: 0x0003c9 group: greek \ code: 0x000393 group: greek \ code: 0x000394 group: greek \ code: 0x000398 group: greek \ code: 0x00039b group: greek \ code: 0x00039e group: greek \ code: 0x0003a0 group: greek \ code: 0x0003a3 group: greek \ code: 0x0003a5 group: greek \ code: 0x0003a6 group: greek \ code: 0x0003a8 group: greek \ code: 0x0003a9 group: greek \ code: 0x01d539 group: letter \ code: 0x002102 group: letter \ code: 0x002115 group: letter \ code: 0x00211a group: letter \ code: 0x00211d group: letter \ code: 0x002124 group: letter \ code: 0x002190 group: arrow abbrev: <. \ code: 0x0027f5 group: arrow abbrev: <. \ code: 0x00290e group: arrow abbrev: <. \ code: 0x0021e0 group: arrow abbrev: <. \ code: 0x002192 group: arrow abbrev: .> abbrev: -> \ code: 0x0027f6 group: arrow abbrev: .> abbrev: --> \ code: 0x00290f group: arrow abbrev: .> abbrev: ---> \ code: 0x0021e2 group: arrow abbrev: .> abbrev: ---> \ code: 0x0021d0 group: arrow abbrev: <. \ code: 0x0027f8 group: arrow abbrev: <. \ code: 0x0021da group: arrow abbrev: <. \ code: 0x0021d2 group: arrow abbrev: .> abbrev: => \ code: 0x0027f9 group: arrow abbrev: .> abbrev: ==> \ code: 0x0021db group: arrow abbrev: .> \ code: 0x002194 group: arrow abbrev: <> abbrev: <-> \ code: 0x0027f7 group: arrow abbrev: <> abbrev: <-> abbrev: <--> \ code: 0x0021d4 group: arrow abbrev: <> \ code: 0x0027fa group: arrow abbrev: <> \ code: 0x0021a6 group: arrow abbrev: .> abbrev: |-> \ code: 0x0027fc group: arrow abbrev: .> abbrev: |--> \ code: 0x002500 group: arrow abbrev: <> \ code: 0x002550 group: arrow abbrev: <> \ code: 0x0021a9 group: arrow abbrev: <. \ code: 0x0021aa group: arrow abbrev: .> \ code: 0x0021bd group: arrow abbrev: <. \ code: 0x0021c1 group: arrow abbrev: .> \ code: 0x0021bc group: arrow abbrev: <. \ code: 0x0021c0 group: arrow abbrev: .> \ code: 0x0021cc group: arrow abbrev: <> abbrev: == \ code: 0x00219d group: arrow abbrev: .> abbrev: ~> \ code: 0x0021c3 group: arrow \ code: 0x0021c2 group: arrow \ code: 0x0021bf group: arrow #\ code: 0x0021be group: arrow \ code: 0x0021be group: operator \ code: 0x002237 group: punctuation \ code: 0x002191 group: arrow \ code: 0x0021d1 group: arrow \ code: 0x002193 group: arrow \ code: 0x0021d3 group: arrow \ code: 0x002195 group: arrow \ code: 0x0021d5 group: arrow \ code: 0x0027e8 group: punctuation abbrev: << \ code: 0x0027e9 group: punctuation abbrev: >> \ code: 0x0027ea group: punctuation abbrev: << \ code: 0x0027eb group: punctuation abbrev: >> \ code: 0x002308 group: punctuation abbrev: [. \ code: 0x002309 group: punctuation abbrev: .] \ code: 0x00230a group: punctuation abbrev: [. \ code: 0x00230b group: punctuation abbrev: .] \ code: 0x002987 group: punctuation abbrev: (| \ code: 0x002988 group: punctuation abbrev: |) \ code: 0x0027e6 group: punctuation abbrev: [| \ code: 0x0027e7 group: punctuation abbrev: |] \ code: 0x002983 group: punctuation abbrev: {| \ code: 0x002984 group: punctuation abbrev: |} \ code: 0x0000ab group: punctuation abbrev: << \ code: 0x0000bb group: punctuation abbrev: >> \ code: 0x0022a5 group: logic \ code: 0x0022a4 group: logic \ code: 0x002227 group: logic abbrev: /\ abbrev: & \ code: 0x0022c0 group: logic abbrev: !! \ code: 0x002228 group: logic abbrev: \/ abbrev: | \ code: 0x0022c1 group: logic abbrev: ?? \ code: 0x002200 group: logic abbrev: ! abbrev: ALL \ code: 0x002203 group: logic abbrev: ? abbrev: EX \ code: 0x002204 group: logic abbrev: ~? \ code: 0x0000ac group: logic abbrev: ~ \ code: 0x0025cb group: logic \ code: 0x0025a1 group: logic \ code: 0x0025c7 group: logic \ code: 0x0022c4 group: operator \ code: 0x0022a2 group: relation abbrev: |- \ code: 0x0022a8 group: relation abbrev: |= \ code: 0x0022a9 group: relation abbrev: |- \ code: 0x0022ab group: relation abbrev: |= \ code: 0x0022a3 group: relation abbrev: -| \ code: 0x00221a group: relation \ code: 0x002264 group: relation abbrev: <= \ code: 0x002265 group: relation abbrev: >= \ code: 0x00226a group: relation abbrev: << \ code: 0x00226b group: relation abbrev: >> \ code: 0x002272 group: relation \ code: 0x002273 group: relation \ code: 0x002a85 group: relation \ code: 0x002a86 group: relation \ code: 0x002208 group: relation abbrev: : \ code: 0x002209 group: relation abbrev: ~: \ code: 0x002282 group: relation \ code: 0x002283 group: relation \ code: 0x002286 group: relation abbrev: (= \ code: 0x002287 group: relation abbrev: )= \ code: 0x00228f group: relation \ code: 0x002290 group: relation \ code: 0x002291 group: relation abbrev: [= \ code: 0x002292 group: relation abbrev: ]= \ code: 0x002229 group: operator abbrev: Int \ code: 0x0022c2 group: operator abbrev: Inter abbrev: INT \ code: 0x00222a group: operator abbrev: Un \ code: 0x0022c3 group: operator abbrev: Union abbrev: UN \ code: 0x002294 group: operator \ code: 0x002a06 group: operator abbrev: SUP \ code: 0x002293 group: operator \ code: 0x002a05 group: operator abbrev: INF \ code: 0x002216 group: operator \ code: 0x00221d group: operator \ code: 0x00228e group: operator \ code: 0x002a04 group: operator \ code: 0x002260 group: relation abbrev: ~= \ code: 0x00223c group: relation \ code: 0x002250 group: relation abbrev: .= \ code: 0x002243 group: relation \ code: 0x002248 group: relation \ code: 0x00224d group: relation \ code: 0x002245 group: relation \ code: 0x002323 group: relation \ code: 0x002261 group: relation abbrev: == \ code: 0x002322 group: relation \ code: 0x0022c8 \ code: 0x002a1d \ code: 0x00227a group: relation \ code: 0x00227b group: relation \ code: 0x00227c group: relation \ code: 0x00227d group: relation \ code: 0x002225 group: punctuation abbrev: || \ code: 0x0000a6 group: punctuation abbrev: || \ code: 0x002aff group: punctuation abbrev: || \ code: 0x0000b1 group: operator \ code: 0x002213 group: operator \ code: 0x0000d7 group: operator abbrev: <*> \
code: 0x0000f7 group: operator \ code: 0x0022c5 group: operator \ code: 0x0022c6 group: operator \ code: 0x002219 group: operator \ code: 0x002218 group: operator \ code: 0x002020 \ code: 0x002021 \ code: 0x0022b2 group: relation \ code: 0x0022b3 group: relation \ code: 0x0022b4 group: relation \ code: 0x0022b5 group: relation \ code: 0x0025c3 group: relation \ code: 0x0025b9 group: relation \ code: 0x0025b3 group: relation \ code: 0x00225c group: relation \ code: 0x002295 group: operator \ code: 0x002a01 group: operator \ code: 0x002297 group: operator \ code: 0x002a02 group: operator \ code: 0x002299 group: operator \ code: 0x002a00 group: operator \ code: 0x002296 group: operator \ code: 0x002298 group: operator \ code: 0x002026 group: punctuation abbrev: ... \ code: 0x0022ef group: punctuation \ code: 0x002211 group: operator abbrev: SUM \ code: 0x00220f group: operator abbrev: PROD \ code: 0x002210 group: operator \ code: 0x00221e \ code: 0x00222b group: operator \ code: 0x00222e group: operator \ code: 0x002663 \ code: 0x002662 \ code: 0x002661 \ code: 0x002660 \ code: 0x002135 \ code: 0x002205 \ code: 0x002207 \ code: 0x002202 \ code: 0x00266d \ code: 0x00266e \ code: 0x00266f \ code: 0x002220 \ code: 0x0000a9 \ code: 0x0000ae \ code: 0x002010 group: punctuation \ code: 0x0000af group: operator \ code: 0x0000b7 group: punctuation \ code: 0x0000bc group: digit \ code: 0x0000bd group: digit \ code: 0x0000be group: digit \ code: 0x0000aa \ code: 0x0000ba \
code: 0x0000a7 \ code: 0x0000b6 \ code: 0x0000a1 \ code: 0x0000bf \ code: 0x0020ac \ code: 0x0000a3 \ code: 0x0000a5 \ code: 0x0000a2 \ code: 0x0000a4 \ code: 0x0000b0 \ code: 0x002a3f group: operator \ code: 0x002127 group: operator \ code: 0x0025ca \ code: 0x002118 \ code: 0x002240 group: relation \ code: 0x0000b4 \ code: 0x000131 \ code: 0x0000a8 \ code: 0x0000b8 \ code: 0x0002dd \ code: 0x00291c group: operator abbrev: >>= \ code: 0x002aa2 group: operator abbrev: >> \ code: 0x0003f5 \ code: 0x002311 \ code: 0x0023ce \ code: 0x002015 group: document argument: space_cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^cancel> code: 0x002326 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^latex> group: document argument: cartouche \<^marker> code: 0x002710 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \ code: 0x002039 group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: << \ code: 0x00203a group: punctuation font: Isabelle␣DejaVu␣Sans␣Mono abbrev: >> \<^here> code: 0x002302 font: Isabelle␣DejaVu␣Sans␣Mono \<^undefined> code: 0x002756 font: Isabelle␣DejaVu␣Sans␣Mono \<^noindent> code: 0x0021e4 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^smallskip> code: 0x002508 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^medskip> code: 0x002509 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^bigskip> code: 0x002501 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^item> code: 0x0025aa group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^enum> code: 0x0025b8 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^descr> code: 0x0027a7 group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^footnote> code: 0x00204b group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^verbatim> code: 0x0025a9 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^theory_text> code: 0x002b1a group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^emph> code: 0x002217 group: document argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^bold> code: 0x002759 group: control argument: cartouche group: document font: Isabelle␣DejaVu␣Sans␣Mono \<^sub> code: 0x0021e9 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^sup> code: 0x0021e7 group: control font: Isabelle␣DejaVu␣Sans␣Mono \<^bsub> code: 0x0021d8 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_( \<^esub> code: 0x0021d9 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =_) \<^bsup> code: 0x0021d7 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^( \<^esup> code: 0x0021d6 group: control_block font: Isabelle␣DejaVu␣Sans␣Mono abbrev: =^) \<^file> code: 0x01F5CF group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^dir> code: 0x01F5C0 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^url> code: 0x01F310 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^doc> code: 0x01F4D3 group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono \<^assert> \<^binding> argument: cartouche \<^class> argument: cartouche \<^class_syntax> argument: cartouche \<^command_keyword> argument: cartouche \<^const> argument: cartouche \<^const_abbrev> argument: cartouche \<^const_name> argument: cartouche \<^const_syntax> argument: cartouche \<^context> \<^cprop> argument: cartouche \<^cterm> argument: cartouche \<^ctyp> argument: cartouche \<^keyword> argument: cartouche \<^locale> argument: cartouche \<^make_string> \<^method> argument: cartouche \<^named_theorems> argument: cartouche \<^nonterminal> argument: cartouche \<^path> argument: cartouche \<^path_binding> argument: cartouche \<^plugin> argument: cartouche \<^print> \<^prop> argument: cartouche +\<^scala> argument: cartouche +\<^scala_function> argument: cartouche \<^session> argument: cartouche \<^simproc> argument: cartouche \<^sort> argument: cartouche \<^syntax_const> argument: cartouche \<^system_option> argument: cartouche \<^term> argument: cartouche \<^theory> argument: cartouche \<^theory_context> argument: cartouche \<^typ> argument: cartouche \<^type_abbrev> argument: cartouche \<^type_name> argument: cartouche \<^type_syntax> argument: cartouche \<^oracle_name> argument: cartouche \<^code> argument: cartouche \<^computation> argument: cartouche \<^computation_conv> argument: cartouche \<^computation_check> argument: cartouche diff --git a/lib/texinputs/isabellesym.sty b/lib/texinputs/isabellesym.sty --- a/lib/texinputs/isabellesym.sty +++ b/lib/texinputs/isabellesym.sty @@ -1,421 +1,423 @@ %% %% definitions of standard Isabelle symbols %% \newcommand{\isasymzero}{\isamath{\mathbf{0}}} %requires amssymb \newcommand{\isasymone}{\isamath{\mathbf{1}}} %requires amssymb \newcommand{\isasymtwo}{\isamath{\mathbf{2}}} %requires amssymb \newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssymb \newcommand{\isasymfour}{\isamath{\mathbf{4}}} %requires amssymb \newcommand{\isasymfive}{\isamath{\mathbf{5}}} %requires amssymb \newcommand{\isasymsix}{\isamath{\mathbf{6}}} %requires amssymb \newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssymb \newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssymb \newcommand{\isasymnine}{\isamath{\mathbf{9}}} %requires amssymb \newcommand{\isasymA}{\isamath{\mathcal{A}}} \newcommand{\isasymB}{\isamath{\mathcal{B}}} \newcommand{\isasymC}{\isamath{\mathcal{C}}} \newcommand{\isasymD}{\isamath{\mathcal{D}}} \newcommand{\isasymE}{\isamath{\mathcal{E}}} \newcommand{\isasymF}{\isamath{\mathcal{F}}} \newcommand{\isasymG}{\isamath{\mathcal{G}}} \newcommand{\isasymH}{\isamath{\mathcal{H}}} \newcommand{\isasymI}{\isamath{\mathcal{I}}} \newcommand{\isasymJ}{\isamath{\mathcal{J}}} \newcommand{\isasymK}{\isamath{\mathcal{K}}} \newcommand{\isasymL}{\isamath{\mathcal{L}}} \newcommand{\isasymM}{\isamath{\mathcal{M}}} \newcommand{\isasymN}{\isamath{\mathcal{N}}} \newcommand{\isasymO}{\isamath{\mathcal{O}}} \newcommand{\isasymP}{\isamath{\mathcal{P}}} \newcommand{\isasymQ}{\isamath{\mathcal{Q}}} \newcommand{\isasymR}{\isamath{\mathcal{R}}} \newcommand{\isasymS}{\isamath{\mathcal{S}}} \newcommand{\isasymT}{\isamath{\mathcal{T}}} \newcommand{\isasymU}{\isamath{\mathcal{U}}} \newcommand{\isasymV}{\isamath{\mathcal{V}}} \newcommand{\isasymW}{\isamath{\mathcal{W}}} \newcommand{\isasymX}{\isamath{\mathcal{X}}} \newcommand{\isasymY}{\isamath{\mathcal{Y}}} \newcommand{\isasymZ}{\isamath{\mathcal{Z}}} \newcommand{\isasyma}{\isamath{\mathrm{a}}} \newcommand{\isasymb}{\isamath{\mathrm{b}}} \newcommand{\isasymc}{\isamath{\mathrm{c}}} \newcommand{\isasymd}{\isamath{\mathrm{d}}} \newcommand{\isasyme}{\isamath{\mathrm{e}}} \newcommand{\isasymf}{\isamath{\mathrm{f}}} \newcommand{\isasymg}{\isamath{\mathrm{g}}} \newcommand{\isasymh}{\isamath{\mathrm{h}}} \newcommand{\isasymi}{\isamath{\mathrm{i}}} \newcommand{\isasymj}{\isamath{\mathrm{j}}} \newcommand{\isasymk}{\isamath{\mathrm{k}}} \newcommand{\isasyml}{\isamath{\mathrm{l}}} \newcommand{\isasymm}{\isamath{\mathrm{m}}} \newcommand{\isasymn}{\isamath{\mathrm{n}}} \newcommand{\isasymo}{\isamath{\mathrm{o}}} \newcommand{\isasymp}{\isamath{\mathrm{p}}} \newcommand{\isasymq}{\isamath{\mathrm{q}}} \newcommand{\isasymr}{\isamath{\mathrm{r}}} \newcommand{\isasyms}{\isamath{\mathrm{s}}} \newcommand{\isasymt}{\isamath{\mathrm{t}}} \newcommand{\isasymu}{\isamath{\mathrm{u}}} \newcommand{\isasymv}{\isamath{\mathrm{v}}} \newcommand{\isasymw}{\isamath{\mathrm{w}}} \newcommand{\isasymx}{\isamath{\mathrm{x}}} \newcommand{\isasymy}{\isamath{\mathrm{y}}} \newcommand{\isasymz}{\isamath{\mathrm{z}}} \newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak \newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak \newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak \newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak \newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak \newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak \newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak \newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak \newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak \newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak \newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak \newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak \newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak \newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak \newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak \newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak \newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak \newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak \newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak \newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak \newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak \newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak \newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak \newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak \newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak \newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak \newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak \newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak \newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak \newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak \newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak \newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak \newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak \newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak \newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak \newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak \newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak \newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak \newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak \newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak \newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak \newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak \newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak \newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak \newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak \newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak \newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak \newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak \newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak \newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak \newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak \newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak \newcommand{\isasymalpha}{\isamath{\alpha}} \newcommand{\isasymbeta}{\isamath{\beta}} \newcommand{\isasymgamma}{\isamath{\gamma}} \newcommand{\isasymdelta}{\isamath{\delta}} \newcommand{\isasymepsilon}{\isamath{\varepsilon}} \newcommand{\isasymzeta}{\isamath{\zeta}} \newcommand{\isasymeta}{\isamath{\eta}} \newcommand{\isasymtheta}{\isamath{\vartheta}} \newcommand{\isasymiota}{\isamath{\iota}} \newcommand{\isasymkappa}{\isamath{\kappa}} \newcommand{\isasymlambda}{\isamath{\lambda}} \newcommand{\isasymmu}{\isamath{\mu}} \newcommand{\isasymnu}{\isamath{\nu}} \newcommand{\isasymxi}{\isamath{\xi}} \newcommand{\isasympi}{\isamath{\pi}} \newcommand{\isasymrho}{\isamath{\varrho}} \newcommand{\isasymsigma}{\isamath{\sigma}} \newcommand{\isasymtau}{\isamath{\tau}} \newcommand{\isasymupsilon}{\isamath{\upsilon}} \newcommand{\isasymphi}{\isamath{\varphi}} \newcommand{\isasymchi}{\isamath{\chi}} \newcommand{\isasympsi}{\isamath{\psi}} \newcommand{\isasymomega}{\isamath{\omega}} \newcommand{\isasymGamma}{\isamath{\Gamma}} \newcommand{\isasymDelta}{\isamath{\Delta}} \newcommand{\isasymTheta}{\isamath{\Theta}} \newcommand{\isasymLambda}{\isamath{\Lambda}} \newcommand{\isasymXi}{\isamath{\Xi}} \newcommand{\isasymPi}{\isamath{\Pi}} \newcommand{\isasymSigma}{\isamath{\Sigma}} \newcommand{\isasymUpsilon}{\isamath{\Upsilon}} \newcommand{\isasymPhi}{\isamath{\Phi}} \newcommand{\isasymPsi}{\isamath{\Psi}} \newcommand{\isasymOmega}{\isamath{\Omega}} \newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}} \newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}} \newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}} \newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}} \newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}} \newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}} \newcommand{\isasymleftarrow}{\isamath{\leftarrow}} \newcommand{\isasymrightarrow}{\isamath{\rightarrow}} \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}} \newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}} \newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}} %requires amsmath \newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}} %requires amsmath \newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}} %requires amsmath \newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}} \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}} \newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}} \newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}} \newcommand{\isasymLleftarrow}{\isamath{\Lleftarrow}} %requires amssymb \newcommand{\isasymRrightarrow}{\isamath{\Rrightarrow}} %requires amssymb \newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}} \newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}} \newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}} \newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}} \newcommand{\isasymmapsto}{\isamath{\mapsto}} \newcommand{\isasymlongmapsto}{\isamath{\longmapsto}} \newcommand{\isasymmidarrow}{\isamath{\relbar}} \newcommand{\isasymMidarrow}{\isamath{\Relbar}} \newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}} \newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}} \newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}} \newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}} \newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}} \newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}} \newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}} \newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires amssymb \newcommand{\isasymdownharpoonleft}{\isamath{\downharpoonleft}} %requires amssymb \newcommand{\isasymdownharpoonright}{\isamath{\downharpoonright}} %requires amssymb \newcommand{\isasymupharpoonleft}{\isamath{\upharpoonleft}} %requires amssymb \newcommand{\isasymupharpoonright}{\isamath{\upharpoonright}} %requires amssymb \newcommand{\isasymrestriction}{\isamath{\restriction}} %requires amssymb \newcommand{\isasymColon}{\isamath{\mathrel{::}}} \newcommand{\isasymup}{\isamath{\uparrow}} \newcommand{\isasymUp}{\isamath{\Uparrow}} \newcommand{\isasymdown}{\isamath{\downarrow}} \newcommand{\isasymDown}{\isamath{\Downarrow}} \newcommand{\isasymupdown}{\isamath{\updownarrow}} \newcommand{\isasymUpdown}{\isamath{\Updownarrow}} \newcommand{\isasymlangle}{\isamath{\langle}} \newcommand{\isasymrangle}{\isamath{\rangle}} \newcommand{\isasymllangle}{\isamath{\langle\mskip-5mu\langle}} \newcommand{\isasymrrangle}{\isamath{\rangle\mskip-5mu\rangle}} \newcommand{\isasymlceil}{\isamath{\lceil}} \newcommand{\isasymrceil}{\isamath{\rceil}} \newcommand{\isasymlfloor}{\isamath{\lfloor}} \newcommand{\isasymrfloor}{\isamath{\rfloor}} \newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}} \newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}} \newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}} \newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}} \newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}} \newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}} \newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel \newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel \newcommand{\isasymbottom}{\isamath{\bot}} \newcommand{\isasymtop}{\isamath{\top}} \newcommand{\isasymand}{\isamath{\wedge}} \newcommand{\isasymAnd}{\isamath{\bigwedge}} \newcommand{\isasymor}{\isamath{\vee}} \newcommand{\isasymOr}{\isamath{\bigvee}} \newcommand{\isasymforall}{\isamath{\forall\,}} \newcommand{\isasymexists}{\isamath{\exists\,}} \newcommand{\isasymnot}{\isamath{\neg}} \newcommand{\isasymnexists}{\isamath{\nexists\,}} %requires amssymb \newcommand{\isasymcircle}{\isamath{\ocircle}} %requires wasysym \newcommand{\isasymbox}{\isamath{\Box}} %requires amssymb \newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires amssymb \newcommand{\isasymdiamondop}{\isamath{\diamond}} \newcommand{\isasymsurd}{\isamath{\surd}} \newcommand{\isasymturnstile}{\isamath{\vdash}} \newcommand{\isasymTurnstile}{\isamath{\models}} \newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}} \newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}} \newcommand{\isasymstileturn}{\isamath{\dashv}} \newcommand{\isasymle}{\isamath{\le}} \newcommand{\isasymge}{\isamath{\ge}} \newcommand{\isasymlless}{\isamath{\ll}} \newcommand{\isasymggreater}{\isamath{\gg}} \newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb \newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb \newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb \newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb \newcommand{\isasymin}{\isamath{\in}} \newcommand{\isasymnotin}{\isamath{\notin}} \newcommand{\isasymsubset}{\isamath{\subset}} \newcommand{\isasymsupset}{\isamath{\supset}} \newcommand{\isasymsubseteq}{\isamath{\subseteq}} \newcommand{\isasymsupseteq}{\isamath{\supseteq}} \newcommand{\isasymsqsubset}{\isamath{\sqsubset}} %requires amssymb \newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires amssymb \newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}} \newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}} \newcommand{\isasyminter}{\isamath{\cap}} \newcommand{\isasymInter}{\isamath{\bigcap\,}} \newcommand{\isasymunion}{\isamath{\cup}} \newcommand{\isasymUnion}{\isamath{\bigcup\,}} \newcommand{\isasymsqunion}{\isamath{\sqcup}} \newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}} \newcommand{\isasymsqinter}{\isamath{\sqcap}} \newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd \newcommand{\isasymsetminus}{\isamath{\setminus}} \newcommand{\isasympropto}{\isamath{\propto}} \newcommand{\isasymuplus}{\isamath{\uplus}} \newcommand{\isasymUplus}{\isamath{\biguplus\,}} \newcommand{\isasymnoteq}{\isamath{\not=}} \newcommand{\isasymsim}{\isamath{\sim}} \newcommand{\isasymdoteq}{\isamath{\doteq}} \newcommand{\isasymsimeq}{\isamath{\simeq}} \newcommand{\isasymapprox}{\isamath{\approx}} \newcommand{\isasymasymp}{\isamath{\asymp}} \newcommand{\isasymcong}{\isamath{\cong}} \newcommand{\isasymsmile}{\isamath{\smile}} \newcommand{\isasymequiv}{\isamath{\equiv}} \newcommand{\isasymfrown}{\isamath{\frown}} \newcommand{\isasymJoin}{\isamath{\Join}} %requires amssymb \newcommand{\isasymbowtie}{\isamath{\bowtie}} \newcommand{\isasymprec}{\isamath{\prec}} \newcommand{\isasymsucc}{\isamath{\succ}} \newcommand{\isasympreceq}{\isamath{\preceq}} \newcommand{\isasymsucceq}{\isamath{\succeq}} \newcommand{\isasymparallel}{\isamath{\parallel}} \newcommand{\isasymbar}{\isamath{\mid}} \newcommand{\isasymbbar}{\isamath{[\mskip-1.5mu]}} \newcommand{\isasymplusminus}{\isamath{\pm}} \newcommand{\isasymminusplus}{\isamath{\mp}} \newcommand{\isasymtimes}{\isamath{\times}} \newcommand{\isasymdiv}{\isamath{\div}} \newcommand{\isasymcdot}{\isamath{\cdot}} \newcommand{\isasymsqdot}{\isamath{\sbox\z@{$\centerdot$}\ht\z@=.33333\ht\z@\vcenter{\box\z@}}} %requires amssymb \newcommand{\isasymstar}{\isamath{\star}} \newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}} \newcommand{\isasymcirc}{\isamath{\circ}} \newcommand{\isasymdagger}{\isamath{\dagger}} \newcommand{\isasymddagger}{\isamath{\ddagger}} \newcommand{\isasymlhd}{\isamath{\lhd}} %requires amssymb \newcommand{\isasymrhd}{\isamath{\rhd}} %requires amssymb \newcommand{\isasymunlhd}{\isamath{\unlhd}} %requires amssymb \newcommand{\isasymunrhd}{\isamath{\unrhd}} %requires amssymb \newcommand{\isasymtriangleleft}{\isamath{\triangleleft}} \newcommand{\isasymtriangleright}{\isamath{\triangleright}} \newcommand{\isasymtriangle}{\isamath{\triangle}} \newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb \newcommand{\isasymoplus}{\isamath{\oplus}} \newcommand{\isasymOplus}{\isamath{\bigoplus\,}} \newcommand{\isasymotimes}{\isamath{\otimes}} \newcommand{\isasymOtimes}{\isamath{\bigotimes\,}} \newcommand{\isasymodot}{\isamath{\odot}} \newcommand{\isasymOdot}{\isamath{\bigodot\,}} \newcommand{\isasymominus}{\isamath{\ominus}} \newcommand{\isasymoslash}{\isamath{\oslash}} \newcommand{\isasymdots}{\isamath{\dots}} \newcommand{\isasymcdots}{\isamath{\cdots}} \newcommand{\isasymSum}{\isamath{\sum\,}} \newcommand{\isasymProd}{\isamath{\prod\,}} \newcommand{\isasymCoprod}{\isamath{\coprod\,}} \newcommand{\isasyminfinity}{\isamath{\infty}} \newcommand{\isasymintegral}{\isamath{\int\,}} \newcommand{\isasymointegral}{\isamath{\oint\,}} \newcommand{\isasymclubsuit}{\isamath{\clubsuit}} \newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}} \newcommand{\isasymheartsuit}{\isamath{\heartsuit}} \newcommand{\isasymspadesuit}{\isamath{\spadesuit}} \newcommand{\isasymaleph}{\isamath{\aleph}} \newcommand{\isasymemptyset}{\isamath{\emptyset}} \newcommand{\isasymnabla}{\isamath{\nabla}} \newcommand{\isasympartial}{\isamath{\partial}} \newcommand{\isasymRe}{\isamath{\Re}} \newcommand{\isasymIm}{\isamath{\Im}} \newcommand{\isasymflat}{\isamath{\flat}} \newcommand{\isasymnatural}{\isamath{\natural}} \newcommand{\isasymsharp}{\isamath{\sharp}} \newcommand{\isasymangle}{\isamath{\angle}} \newcommand{\isasymcopyright}{\isatext{\normalfont\rmfamily\copyright}} \newcommand{\isasymregistered}{\isatext{\normalfont\rmfamily\textregistered}} \newcommand{\isasyminverse}{\isamath{{}^{-1}}} \newcommand{\isasymonequarter}{\isatext{\normalfont\rmfamily\textonequarter}} %requires textcomp \newcommand{\isasymonehalf}{\isatext{\normalfont\rmfamily\textonehalf}} %requires textcomp \newcommand{\isasymthreequarters}{\isatext{\normalfont\rmfamily\textthreequarters}} %requires textcomp \newcommand{\isasymordfeminine}{\isatext{\normalfont\rmfamily\textordfeminine}} \newcommand{\isasymordmasculine}{\isatext{\normalfont\rmfamily\textordmasculine}} \newcommand{\isasymsection}{\isatext{\normalfont\rmfamily\S}} \newcommand{\isasymparagraph}{\isatext{\normalfont\rmfamily\P}} \newcommand{\isasymexclamdown}{\isatext{\normalfont\rmfamily\textexclamdown}} \newcommand{\isasymquestiondown}{\isatext{\normalfont\rmfamily\textquestiondown}} \newcommand{\isasymeuro}{\isatext{\euro}} %requires eurosym \newcommand{\isasympounds}{\isamath{\pounds}} \newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb \newcommand{\isasymcent}{\isatext{\textcent}} %requires textcomp \newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp \newcommand{\isasymdegree}{\isatext{\normalfont\rmfamily\textdegree}} %requires textcomp \newcommand{\isasymhyphen}{\isatext{\normalfont\rmfamily-}} \newcommand{\isasymamalg}{\isamath{\amalg}} \newcommand{\isasymmho}{\isamath{\mho}} %requires amssymb \newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssymb \newcommand{\isasymwp}{\isamath{\wp}} \newcommand{\isasymwrong}{\isamath{\wr}} \newcommand{\isasymacute}{\isatext{\'\relax}} \newcommand{\isasymindex}{\isatext{\i}} \newcommand{\isasymdieresis}{\isatext{\"\relax}} \newcommand{\isasymcedilla}{\isatext{\c\relax}} \newcommand{\isasymhungarumlaut}{\isatext{\H\relax}} \newcommand{\isasymsome}{\isamath{\epsilon\,}} \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}} \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}} \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}} \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}} \newcommand{\isasymhole}{\isatext{\normalfont\rmfamily\wasylozenge}} %requires wasysym \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}} \newcommand{\isasymcomment}{\isatext{\isastylecmt---}} \newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}} \newcommand{\isactrlmarker}{\isatext{\ding{48}}} %requires pifont \newcommand{\isactrlassert}{\isakeywordcontrol{assert}} \newcommand{\isactrlcancel}{\isakeywordcontrol{cancel}} \newcommand{\isactrlbinding}{\isakeywordcontrol{binding}} \newcommand{\isactrlclass}{\isakeywordcontrol{class}} \newcommand{\isactrlclassUNDERSCOREsyntax}{\isakeywordcontrol{class{\isacharunderscore}syntax}} \newcommand{\isactrlcommandUNDERSCOREkeyword}{\isakeywordcontrol{command{\isacharunderscore}keyword}} \newcommand{\isactrlconst}{\isakeywordcontrol{const}} \newcommand{\isactrlconstUNDERSCOREabbrev}{\isakeywordcontrol{const{\isacharunderscore}abbrev}} \newcommand{\isactrlconstUNDERSCOREname}{\isakeywordcontrol{const{\isacharunderscore}name}} \newcommand{\isactrlconstUNDERSCOREsyntax}{\isakeywordcontrol{const{\isacharunderscore}syntax}} \newcommand{\isactrlcontext}{\isakeywordcontrol{context}} \newcommand{\isactrlcprop}{\isakeywordcontrol{cprop}} \newcommand{\isactrlcterm}{\isakeywordcontrol{cterm}} \newcommand{\isactrlctyp}{\isakeywordcontrol{ctyp}} \newcommand{\isactrldir}{\isakeywordcontrol{dir}} \newcommand{\isactrlfile}{\isakeywordcontrol{file}} \newcommand{\isactrlhere}{\isakeywordcontrol{here}} \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}} \newcommand{\isactrllatex}{\isakeywordcontrol{latex}} \newcommand{\isactrllocale}{\isakeywordcontrol{locale}} \newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}} \newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}} \newcommand{\isactrlmethod}{\isakeywordcontrol{method}} \newcommand{\isactrlnamedUNDERSCOREtheorems}{\isakeywordcontrol{named{\isacharunderscore}theorems}} \newcommand{\isactrlnonterminal}{\isakeywordcontrol{nonterminal}} \newcommand{\isactrlpath}{\isakeywordcontrol{path}} \newcommand{\isactrlpathUNDERSCOREbinding}{\isakeywordcontrol{path{\isacharunderscore}binding}} \newcommand{\isactrlplugin}{\isakeywordcontrol{plugin}} \newcommand{\isactrlprint}{\isakeywordcontrol{print}} \newcommand{\isactrlprop}{\isakeywordcontrol{prop}} +\newcommand{\isactrlscala}{\isakeywordcontrol{scala}} +\newcommand{\isactrlscalaUNDERSCOREfunction}{\isakeywordcontrol{scala{\isacharunderscore}function}} \newcommand{\isactrlsimproc}{\isakeywordcontrol{simproc}} \newcommand{\isactrlsort}{\isakeywordcontrol{sort}} \newcommand{\isactrlsyntaxUNDERSCOREconst}{\isakeywordcontrol{syntax{\isacharunderscore}const}} \newcommand{\isactrlsystemUNDERSCOREoption}{\isakeywordcontrol{system{\isacharunderscore}option}} \newcommand{\isactrlterm}{\isakeywordcontrol{term}} \newcommand{\isactrltheory}{\isakeywordcontrol{theory}} \newcommand{\isactrltheoryUNDERSCOREcontext}{\isakeywordcontrol{theory{\isacharunderscore}context}} \newcommand{\isactrltyp}{\isakeywordcontrol{typ}} \newcommand{\isactrltypeUNDERSCOREabbrev}{\isakeywordcontrol{type{\isacharunderscore}abbrev}} \newcommand{\isactrltypeUNDERSCOREname}{\isakeywordcontrol{type{\isacharunderscore}name}} \newcommand{\isactrltypeUNDERSCOREsyntax}{\isakeywordcontrol{type{\isacharunderscore}syntax}} \newcommand{\isactrlundefined}{\isakeywordcontrol{undefined}} \newcommand{\isactrlcode}{\isakeywordcontrol{code}} \newcommand{\isactrlcomputation}{\isakeywordcontrol{computation}} \newcommand{\isactrlcomputationUNDERSCOREconv}{\isakeywordcontrol{computation{\isacharunderscore}conv}} \newcommand{\isactrlcomputationUNDERSCOREcheck}{\isakeywordcontrol{computation{\isacharunderscore}check}} diff --git a/src/Pure/ML/ml_process.scala b/src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala +++ b/src/Pure/ML/ml_process.scala @@ -1,193 +1,195 @@ /* Title: Pure/ML/ml_process.scala Author: Makarius The raw ML process. */ package isabelle import java.io.{File => JFile} object ML_Process { def apply(options: Options, sessions_structure: Sessions.Structure, store: Sessions.Store, logic: String = "", raw_ml_system: Boolean = false, use_prelude: List[String] = Nil, eval_main: String = "", args: List[String] = Nil, modes: List[String] = Nil, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), redirect: Boolean = false, cleanup: () => Unit = () => (), session_base: Option[Sessions.Base] = None): Bash.Process = { val logic_name = Isabelle_System.default_logic(logic) val heaps: List[String] = if (raw_ml_system) Nil else { sessions_structure.selection(Sessions.Selection.session(logic_name)). build_requirements(List(logic_name)). map(a => File.platform_path(store.the_heap(a))) } val eval_init = if (heaps.isEmpty) { List( """ fun chapter (_: string) = (); fun section (_: string) = (); fun subsection (_: string) = (); fun subsubsection (_: string) = (); fun paragraph (_: string) = (); fun subparagraph (_: string) = (); val ML_file = PolyML.use; """, if (Platform.is_windows) "fun exit 0 = OS.Process.exit OS.Process.success" + " | exit 1 = OS.Process.exit OS.Process.failure" + " | exit rc = OS.Process.exit (RunCall.unsafeCast (Word8.fromInt rc))" else "fun exit rc = Posix.Process.exit (Word8.fromInt rc)", "PolyML.Compiler.prompt1 := \"Poly/ML> \"", "PolyML.Compiler.prompt2 := \"Poly/ML# \"") } else List( "(PolyML.SaveState.loadHierarchy " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(heaps) + "; PolyML.print_depth 0) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ " + ML_Syntax.print_string_bytes(": " + logic_name + "\n") + "); OS.Process.exit OS.Process.failure)") val eval_modes = if (modes.isEmpty) Nil else List("Print_Mode.add_modes " + ML_Syntax.print_list(ML_Syntax.print_string_bytes)(modes)) // options val isabelle_process_options = Isabelle_System.tmp_file("options") Isabelle_System.chmod("600", File.path(isabelle_process_options)) File.write(isabelle_process_options, YXML.string_of_body(options.encode)) val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options)) val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()") // session base val eval_session_base = session_base match { case None => Nil case Some(base) => def print_table(table: List[(String, String)]): String = ML_Syntax.print_list( ML_Syntax.print_pair( ML_Syntax.print_string_bytes, ML_Syntax.print_string_bytes))(table) def print_list(list: List[String]): String = ML_Syntax.print_list(ML_Syntax.print_string_bytes)(list) def print_sessions(list: List[(String, Position.T)]): String = ML_Syntax.print_list( ML_Syntax.print_pair(ML_Syntax.print_string_bytes, ML_Syntax.print_properties))(list) List("Resources.init_session" + "{pide = false" + ", session_positions = " + print_sessions(sessions_structure.session_positions) + ", session_directories = " + print_table(sessions_structure.dest_session_directories) + ", docs = " + print_list(base.doc_names) + ", global_theories = " + print_table(base.global_theories.toList) + ", loaded_theories = " + print_list(base.loaded_theories.keys) + "}") } // process val eval_process = proper_string(eval_main).getOrElse( if (heaps.isEmpty) { "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")) } else "Isabelle_Process.init ()") // ISABELLE_TMP val isabelle_tmp = Isabelle_System.tmp_dir("process") val env_tmp = Map("ISABELLE_TMP" -> File.standard_path(isabelle_tmp)) + val env_functions = Map("ISABELLE_SCALA_FUNCTIONS" -> Scala.functions.mkString(",")) + val ml_runtime_options = { val ml_options = Word.explode(Isabelle_System.getenv("ML_OPTIONS")) val ml_options1 = if (ml_options.exists(_.containsSlice("gcthreads"))) ml_options else ml_options ::: List("--gcthreads", options.int("threads").toString) val ml_options2 = if (!Platform.is_windows || ml_options.exists(_.containsSlice("codepage"))) ml_options1 else ml_options1 ::: List("--codepage", "utf8") ml_options2 } // bash val bash_args = ml_runtime_options ::: (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) ::: use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + Bash.strings(bash_args), cwd = cwd, - env = env ++ env_options ++ env_tmp, + env = env ++ env_options ++ env_tmp ++ env_functions, redirect = redirect, cleanup = () => { isabelle_process_options.delete Isabelle_System.rm_tree(isabelle_tmp) cleanup() }) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("process", "raw ML process (batch mode)", args => { var dirs: List[Path] = Nil var eval_args: List[String] = Nil var logic = Isabelle_System.getenv("ISABELLE_LOGIC") var modes: List[String] = Nil var options = Options.init() val getopts = Getopts(""" Usage: isabelle process [OPTIONS] Options are: -T THEORY load theory -d DIR include session directory -e ML_EXPR evaluate ML expression on startup -f ML_FILE evaluate ML file on startup -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) -m MODE add print mode for output -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) Run the raw Isabelle ML process in batch mode. """, "T:" -> (arg => eval_args = eval_args ::: List("--eval", "use_thy " + ML_Syntax.print_string_bytes(arg))), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "e:" -> (arg => eval_args = eval_args ::: List("--eval", arg)), "f:" -> (arg => eval_args = eval_args ::: List("--use", arg)), "l:" -> (arg => logic = arg), "m:" -> (arg => modes = arg :: modes), "o:" -> (arg => options = options + arg)) val more_args = getopts(args) if (args.isEmpty || more_args.nonEmpty) getopts.usage() val sessions_structure = Sessions.load_structure(options, dirs = dirs) val store = Sessions.store(options) val rc = ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes) .result().print_stdout.rc sys.exit(rc) }) } diff --git a/src/Pure/PIDE/markup.ML b/src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML +++ b/src/Pure/PIDE/markup.ML @@ -1,794 +1,796 @@ (* Title: Pure/PIDE/markup.ML Author: Makarius Quasi-abstract markup elements. *) signature MARKUP = sig type T = string * Properties.T val empty: T val is_empty: T -> bool val properties: Properties.T -> T -> T val nameN: string val name: string -> T -> T val xnameN: string val xname: string -> T -> T val kindN: string val serialN: string val serial_properties: int -> Properties.T val instanceN: string val meta_titleN: string val meta_title: T val meta_creatorN: string val meta_creator: T val meta_contributorN: string val meta_contributor: T val meta_dateN: string val meta_date: T val meta_licenseN: string val meta_license: T val meta_descriptionN: string val meta_description: T val languageN: string val symbolsN: string val delimitedN: string val is_delimited: Properties.T -> bool val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T val language_Isar: bool -> T val language_method: T val language_attribute: T val language_sort: bool -> T val language_type: bool -> T val language_term: bool -> T val language_prop: bool -> T val language_ML: bool -> T val language_SML: bool -> T val language_document: bool -> T val language_document_marker: T val language_antiquotation: T val language_text: bool -> T val language_verbatim: bool -> T val language_latex: bool -> T val language_rail: T val language_path: T val language_mixfix: T val bindingN: string val binding: T val entityN: string val entity: string -> string -> T val defN: string val refN: string val completionN: string val completion: T val no_completionN: string val no_completion: T val updateN: string val update: T val lineN: string val end_lineN: string val offsetN: string val end_offsetN: string val fileN: string val idN: string val position_properties': string list val position_properties: string list val positionN: string val position: T val expressionN: string val expression: string -> T val citationN: string val citation: string -> T val pathN: string val path: string -> T val export_pathN: string val export_path: string -> T val urlN: string val url: string -> T val docN: string val doc: string -> T + val scala_functionN: string val scala_function: string -> T val markupN: string val consistentN: string val unbreakableN: string val block_properties: string list val indentN: string val widthN: string val blockN: string val block: bool -> int -> T val breakN: string val break: int -> int -> T val fbreakN: string val fbreak: T val itemN: string val item: T val wordsN: string val words: T val hiddenN: string val hidden: T val deleteN: string val delete: T val system_optionN: string val sessionN: string val theoryN: string val classN: string val type_nameN: string val constantN: string val fixedN: string val fixed: string -> T val caseN: string val case_: string -> T val dynamic_factN: string val dynamic_fact: string -> T val literal_factN: string val literal_fact: string -> T val method_modifierN: string val tfreeN: string val tfree: T val tvarN: string val tvar: T val freeN: string val free: T val skolemN: string val skolem: T val boundN: string val bound: T val varN: string val var: T val numeralN: string val numeral: T val literalN: string val literal: T val delimiterN: string val delimiter: T val inner_stringN: string val inner_string: T val inner_cartoucheN: string val inner_cartouche: T val token_rangeN: string val token_range: T val sortingN: string val sorting: T val typingN: string val typing: T val class_parameterN: string val class_parameter: T val ML_keyword1N: string val ML_keyword1: T val ML_keyword2N: string val ML_keyword2: T val ML_keyword3N: string val ML_keyword3: T val ML_delimiterN: string val ML_delimiter: T val ML_tvarN: string val ML_tvar: T val ML_numeralN: string val ML_numeral: T val ML_charN: string val ML_char: T val ML_stringN: string val ML_string: T val ML_commentN: string val ML_comment: T val ML_defN: string val ML_openN: string val ML_structureN: string val ML_typingN: string val ML_typing: T val ML_breakpointN: string val ML_breakpoint: int -> T val antiquotedN: string val antiquoted: T val antiquoteN: string val antiquote: T val file_typeN: string val antiquotationN: string val ML_antiquotationN: string val document_antiquotationN: string val document_antiquotation_optionN: string val raw_textN: string val raw_text: T val plain_textN: string val plain_text: T val paragraphN: string val paragraph: T val text_foldN: string val text_fold: T val document_markerN: string val document_marker: T val document_tagN: string val document_tag: string -> T val markdown_paragraphN: string val markdown_paragraph: T val markdown_itemN: string val markdown_item: T val markdown_bulletN: string val markdown_bullet: int -> T val markdown_listN: string val markdown_list: string -> T val itemizeN: string val enumerateN: string val descriptionN: string val inputN: string val input: bool -> Properties.T -> T val command_keywordN: string val command_keyword: T val commandN: string val command_properties: T -> T val keywordN: string val keyword_properties: T -> T val stringN: string val string: T val alt_stringN: string val alt_string: T val verbatimN: string val verbatim: T val cartoucheN: string val cartouche: T val commentN: string val comment: T val keyword1N: string val keyword1: T val keyword2N: string val keyword2: T val keyword3N: string val keyword3: T val quasi_keywordN: string val quasi_keyword: T val improperN: string val improper: T val operatorN: string val operator: T val comment1N: string val comment1: T val comment2N: string val comment2: T val comment3N: string val comment3: T val elapsedN: string val cpuN: string val gcN: string val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T val parse_timing_properties: Properties.T -> {elapsed: Time.time, cpu: Time.time, gc: Time.time} val command_timingN: string val command_timing_properties: {file: string, offset: int, name: string} -> Time.time -> Properties.T val parse_command_timing_properties: Properties.T -> ({file: string, offset: int, name: string} * Time.time) option val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T val command_indentN: string val command_indent: int -> T val goalN: string val goal: T val subgoalN: string val subgoal: string -> T val taskN: string val forkedN: string val forked: T val joinedN: string val joined: T val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T val canceledN: string val canceled: T val initializedN: string val initialized: T val finalizedN: string val finalized: T val consolidatingN: string val consolidating: T val consolidatedN: string val consolidated: T val exec_idN: string val initN: string val statusN: string val status: T val resultN: string val result: T val writelnN: string val writeln: T val stateN: string val state: T val informationN: string val information: T val tracingN: string val tracing: T val warningN: string val warning: T val legacyN: string val legacy: T val errorN: string val error: T val systemN: string val system: T val protocolN: string val reportN: string val report: T val no_reportN: string val no_report: T val badN: string val bad: unit -> T val intensifyN: string val intensify: T val browserN: string val graphviewN: string val theory_exportsN: string val sendbackN: string val paddingN: string val padding_line: Properties.entry val padding_command: Properties.entry val dialogN: string val dialog: serial -> string -> T val jedit_actionN: string val functionN: string val commands_accepted: Properties.T val assign_update: Properties.T val removed_versions: Properties.T val protocol_handler: string -> Properties.T val invoke_scala: string -> string -> Properties.T val cancel_scala: string -> Properties.T val ML_statistics: Properties.entry val task_statistics: Properties.entry val command_timing: Properties.entry val theory_timing: Properties.entry val loading_theory: string -> Properties.T val dest_loading_theory: Properties.T -> string option val build_session_finished: Properties.T val print_operationsN: string val print_operations: Properties.T val exportN: string type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool} val export: export_args -> Properties.T val debugger_state: string -> Properties.T val debugger_output: string -> Properties.T val simp_trace_panelN: string val simp_trace_logN: string val simp_trace_stepN: string val simp_trace_recurseN: string val simp_trace_hintN: string val simp_trace_ignoreN: string val simp_trace_cancel: serial -> Properties.T type output = Output.output * Output.output val no_output: output val add_mode: string -> (T -> output) -> unit val output: T -> output val enclose: T -> Output.output -> Output.output val markup: T -> string -> string val markups: T list -> string -> string val markup_only: T -> string val markup_report: string -> string end; structure Markup: MARKUP = struct (** markup elements **) (* basic markup *) type T = string * Properties.T; val empty = ("", []); fun is_empty ("", _) = true | is_empty _ = false; fun properties more_props ((elem, props): T) = (elem, fold_rev Properties.put more_props props); fun markup_elem name = (name, (name, []): T); fun markup_string name prop = (name, fn s => (name, [(prop, s)]): T); fun markup_int name prop = (name, fn i => (name, [(prop, Value.print_int i)]): T); (* misc properties *) val nameN = "name"; fun name a = properties [(nameN, a)]; val xnameN = "xname"; fun xname a = properties [(xnameN, a)]; val kindN = "kind"; val serialN = "serial"; fun serial_properties i = [(serialN, Value.print_int i)]; val instanceN = "instance"; (* meta data -- see https://www.dublincore.org/specifications/dublin-core/dcmi-terms *) val (meta_titleN, meta_title) = markup_elem "meta_title"; val (meta_creatorN, meta_creator) = markup_elem "meta_creator"; val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor"; val (meta_dateN, meta_date) = markup_elem "meta_date"; val (meta_licenseN, meta_license) = markup_elem "meta_license"; val (meta_descriptionN, meta_description) = markup_elem "meta_description"; (* embedded languages *) val languageN = "language"; val symbolsN = "symbols"; val antiquotesN = "antiquotes"; val delimitedN = "delimited" fun is_delimited props = Properties.get props delimitedN = SOME "true"; fun language {name, symbols, antiquotes, delimited} = (languageN, [(nameN, name), (symbolsN, Value.print_bool symbols), (antiquotesN, Value.print_bool antiquotes), (delimitedN, Value.print_bool delimited)]); fun language' {name, symbols, antiquotes} delimited = language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited}; val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false}; val language_method = language {name = "method", symbols = true, antiquotes = false, delimited = false}; val language_attribute = language {name = "attribute", symbols = true, antiquotes = false, delimited = false}; val language_sort = language' {name = "sort", symbols = true, antiquotes = false}; val language_type = language' {name = "type", symbols = true, antiquotes = false}; val language_term = language' {name = "term", symbols = true, antiquotes = false}; val language_prop = language' {name = "prop", symbols = true, antiquotes = false}; val language_ML = language' {name = "ML", symbols = false, antiquotes = true}; val language_SML = language' {name = "SML", symbols = false, antiquotes = false}; val language_document = language' {name = "document", symbols = false, antiquotes = true}; val language_document_marker = language {name = "document_marker", symbols = true, antiquotes = true, delimited = true}; val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true}; val language_text = language' {name = "text", symbols = true, antiquotes = false}; val language_verbatim = language' {name = "verbatim_text", symbols = true, antiquotes = false}; val language_latex = language' {name = "latex", symbols = false, antiquotes = false}; val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true}; val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true}; val language_mixfix = language {name = "mixfix_annotation", symbols = true, antiquotes = false, delimited = true}; (* formal entities *) val (bindingN, binding) = markup_elem "binding"; val entityN = "entity"; fun entity kind name = (entityN, (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)])); val defN = "def"; val refN = "ref"; (* completion *) val (completionN, completion) = markup_elem "completion"; val (no_completionN, no_completion) = markup_elem "no_completion"; val (updateN, update) = markup_elem "update"; (* position *) val lineN = "line"; val end_lineN = "end_line"; val offsetN = "offset"; val end_offsetN = "end_offset"; val fileN = "file"; val idN = "id"; val position_properties' = [fileN, idN]; val position_properties = [lineN, offsetN, end_offsetN] @ position_properties'; val (positionN, position) = markup_elem "position"; (* expression *) val expressionN = "expression"; fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]); (* citation *) val (citationN, citation) = markup_string "citation" nameN; (* external resources *) val (pathN, path) = markup_string "path" nameN; val (export_pathN, export_path) = markup_string "export_path" nameN; val (urlN, url) = markup_string "url" nameN; val (docN, doc) = markup_string "doc" nameN; +val (scala_functionN, scala_function) = markup_string "scala_function" nameN; (* pretty printing *) val markupN = "markup"; val consistentN = "consistent"; val unbreakableN = "unbreakable"; val indentN = "indent"; val block_properties = [markupN, consistentN, unbreakableN, indentN]; val widthN = "width"; val blockN = "block"; fun block c i = (blockN, (if c then [(consistentN, Value.print_bool c)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val breakN = "break"; fun break w i = (breakN, (if w <> 0 then [(widthN, Value.print_int w)] else []) @ (if i <> 0 then [(indentN, Value.print_int i)] else [])); val (fbreakN, fbreak) = markup_elem "fbreak"; val (itemN, item) = markup_elem "item"; (* text properties *) val (wordsN, words) = markup_elem "words"; val (hiddenN, hidden) = markup_elem "hidden"; val (deleteN, delete) = markup_elem "delete"; (* misc entities *) val system_optionN = "system_option"; val sessionN = "session"; val theoryN = "theory"; val classN = "class"; val type_nameN = "type_name"; val constantN = "constant"; val (fixedN, fixed) = markup_string "fixed" nameN; val (caseN, case_) = markup_string "case" nameN; val (dynamic_factN, dynamic_fact) = markup_string "dynamic_fact" nameN; val (literal_factN, literal_fact) = markup_string "literal_fact" nameN; val method_modifierN = "method_modifier"; (* inner syntax *) val (tfreeN, tfree) = markup_elem "tfree"; val (tvarN, tvar) = markup_elem "tvar"; val (freeN, free) = markup_elem "free"; val (skolemN, skolem) = markup_elem "skolem"; val (boundN, bound) = markup_elem "bound"; val (varN, var) = markup_elem "var"; val (numeralN, numeral) = markup_elem "numeral"; val (literalN, literal) = markup_elem "literal"; val (delimiterN, delimiter) = markup_elem "delimiter"; val (inner_stringN, inner_string) = markup_elem "inner_string"; val (inner_cartoucheN, inner_cartouche) = markup_elem "inner_cartouche"; val (token_rangeN, token_range) = markup_elem "token_range"; val (sortingN, sorting) = markup_elem "sorting"; val (typingN, typing) = markup_elem "typing"; val (class_parameterN, class_parameter) = markup_elem "class_parameter"; (* ML *) val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1"; val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2"; val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3"; val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter"; val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar"; val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral"; val (ML_charN, ML_char) = markup_elem "ML_char"; val (ML_stringN, ML_string) = markup_elem "ML_string"; val (ML_commentN, ML_comment) = markup_elem "ML_comment"; val ML_defN = "ML_def"; val ML_openN = "ML_open"; val ML_structureN = "ML_structure"; val (ML_typingN, ML_typing) = markup_elem "ML_typing"; val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN; (* antiquotations *) val (antiquotedN, antiquoted) = markup_elem "antiquoted"; val (antiquoteN, antiquote) = markup_elem "antiquote"; val file_typeN = "file_type"; val antiquotationN = "antiquotation"; val ML_antiquotationN = "ML_antiquotation"; val document_antiquotationN = "document_antiquotation"; val document_antiquotation_optionN = "document_antiquotation_option"; (* document text *) val (raw_textN, raw_text) = markup_elem "raw_text"; val (plain_textN, plain_text) = markup_elem "plain_text"; val (paragraphN, paragraph) = markup_elem "paragraph"; val (text_foldN, text_fold) = markup_elem "text_fold"; val (document_markerN, document_marker) = markup_elem "document_marker"; val (document_tagN, document_tag) = markup_string "document_tag" nameN; (* Markdown document structure *) val (markdown_paragraphN, markdown_paragraph) = markup_elem "markdown_paragraph"; val (markdown_itemN, markdown_item) = markup_elem "markdown_item"; val (markdown_bulletN, markdown_bullet) = markup_int "markdown_bullet" "depth"; val (markdown_listN, markdown_list) = markup_string "markdown_list" kindN; val itemizeN = "itemize"; val enumerateN = "enumerate"; val descriptionN = "description"; (* formal input *) val inputN = "input"; fun input delimited props = (inputN, (delimitedN, Value.print_bool delimited) :: props); (* outer syntax *) val (command_keywordN, command_keyword) = markup_elem "command_keyword"; val commandN = "command"; val command_properties = properties [(kindN, commandN)]; val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)]; val (keyword1N, keyword1) = markup_elem "keyword1"; val (keyword2N, keyword2) = markup_elem "keyword2"; val (keyword3N, keyword3) = markup_elem "keyword3"; val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword"; val (improperN, improper) = markup_elem "improper"; val (operatorN, operator) = markup_elem "operator"; val (stringN, string) = markup_elem "string"; val (alt_stringN, alt_string) = markup_elem "alt_string"; val (verbatimN, verbatim) = markup_elem "verbatim"; val (cartoucheN, cartouche) = markup_elem "cartouche"; val (commentN, comment) = markup_elem "comment"; (* comments *) val (comment1N, comment1) = markup_elem "comment1"; val (comment2N, comment2) = markup_elem "comment2"; val (comment3N, comment3) = markup_elem "comment3"; (* timing *) val elapsedN = "elapsed"; val cpuN = "cpu"; val gcN = "gc"; fun timing_properties {elapsed, cpu, gc} = [(elapsedN, Value.print_time elapsed), (cpuN, Value.print_time cpu), (gcN, Value.print_time gc)]; fun parse_timing_properties props = {elapsed = Properties.seconds props elapsedN, cpu = Properties.seconds props cpuN, gc = Properties.seconds props gcN}; val timingN = "timing"; fun timing t = (timingN, timing_properties t); (* command timing *) val command_timingN = "command_timing"; fun command_timing_properties {file, offset, name} elapsed = [(fileN, file), (offsetN, Value.print_int offset), (nameN, name), (elapsedN, Value.print_time elapsed)]; fun parse_command_timing_properties props = (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of (SOME file, SOME offset, SOME name) => SOME ({file = file, offset = Value.parse_int offset, name = name}, Properties.seconds props elapsedN) | _ => NONE); (* indentation *) val (command_indentN, command_indent) = markup_int "command_indent" indentN; (* goals *) val (goalN, goal) = markup_elem "goal"; val (subgoalN, subgoal) = markup_string "subgoal" nameN; (* command status *) val taskN = "task"; val (forkedN, forked) = markup_elem "forked"; val (joinedN, joined) = markup_elem "joined"; val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; val (canceledN, canceled) = markup_elem "canceled"; val (initializedN, initialized) = markup_elem "initialized"; val (finalizedN, finalized) = markup_elem "finalized"; val (consolidatingN, consolidating) = markup_elem "consolidating"; val (consolidatedN, consolidated) = markup_elem "consolidated"; (* messages *) val exec_idN = "exec_id"; val initN = "init"; val (statusN, status) = markup_elem "status"; val (resultN, result) = markup_elem "result"; val (writelnN, writeln) = markup_elem "writeln"; val (stateN, state) = markup_elem "state" val (informationN, information) = markup_elem "information"; val (tracingN, tracing) = markup_elem "tracing"; val (warningN, warning) = markup_elem "warning"; val (legacyN, legacy) = markup_elem "legacy"; val (errorN, error) = markup_elem "error"; val (systemN, system) = markup_elem "system"; val protocolN = "protocol"; val (reportN, report) = markup_elem "report"; val (no_reportN, no_report) = markup_elem "no_report"; val badN = "bad"; fun bad () = (badN, serial_properties (serial ())); val (intensifyN, intensify) = markup_elem "intensify"; (* active areas *) val browserN = "browser" val graphviewN = "graphview"; val theory_exportsN = "theory_exports"; val sendbackN = "sendback"; val paddingN = "padding"; val padding_line = (paddingN, "line"); val padding_command = (paddingN, "command"); val dialogN = "dialog"; fun dialog i result = (dialogN, [(serialN, Value.print_int i), (resultN, result)]); val jedit_actionN = "jedit_action"; (* protocol message functions *) val functionN = "function" val commands_accepted = [(functionN, "commands_accepted")]; val assign_update = [(functionN, "assign_update")]; val removed_versions = [(functionN, "removed_versions")]; fun protocol_handler name = [(functionN, "protocol_handler"), (nameN, name)]; fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; val ML_statistics = (functionN, "ML_statistics"); val task_statistics = (functionN, "task_statistics"); val command_timing = (functionN, "command_timing"); val theory_timing = (functionN, "theory_timing"); fun loading_theory name = [("function", "loading_theory"), ("name", name)]; fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name | dest_loading_theory _ = NONE; val build_session_finished = [("function", "build_session_finished")]; val print_operationsN = "print_operations"; val print_operations = [(functionN, print_operationsN)]; (* export *) val exportN = "export"; type export_args = {id: string option, serial: serial, theory_name: string, name: string, executable: bool, compress: bool, strict: bool}; fun export ({id, serial, theory_name, name, executable, compress, strict}: export_args) = [(functionN, exportN), (idN, the_default "" id), (serialN, Value.print_int serial), ("theory_name", theory_name), (nameN, name), ("executable", Value.print_bool executable), ("compress", Value.print_bool compress), ("strict", Value.print_bool strict)]; (* debugger *) fun debugger_state name = [(functionN, "debugger_state"), (nameN, name)]; fun debugger_output name = [(functionN, "debugger_output"), (nameN, name)]; (* simplifier trace *) val simp_trace_panelN = "simp_trace_panel"; val simp_trace_logN = "simp_trace_log"; val simp_trace_stepN = "simp_trace_step"; val simp_trace_recurseN = "simp_trace_recurse"; val simp_trace_hintN = "simp_trace_hint"; val simp_trace_ignoreN = "simp_trace_ignore"; fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, Value.print_int i)]; (** print mode operations **) type output = Output.output * Output.output; val no_output = ("", ""); local val default = {output = Output_Primitives.markup_fn}; val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); in fun add_mode name output = Synchronized.change modes (fn tab => (if not (Symtab.defined tab name) then () else Output.warning ("Redefining markup mode " ^ quote name); Symtab.update (name, {output = output}) tab)); fun get_mode () = the_default default (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); end; fun output m = if is_empty m then no_output else #output (get_mode ()) m; val enclose = output #-> Library.enclose; fun markup m = let val (bg, en) = output m in Library.enclose (Output.escape bg) (Output.escape en) end; val markups = fold_rev markup; fun markup_only m = markup m ""; fun markup_report "" = "" | markup_report txt = markup report txt; end; diff --git a/src/Pure/ROOT.ML b/src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML +++ b/src/Pure/ROOT.ML @@ -1,356 +1,357 @@ (* Title: Pure/ROOT.ML Author: Makarius Main entry point for the Isabelle/Pure bootstrap process. Note: When this file is open in the Prover IDE, the ML files of Isabelle/Pure can be explored interactively. This is a separate copy of Pure within Pure: it does not affect the running logic session. *) chapter "Isabelle/Pure bootstrap"; ML_file "ML/ml_name_space.ML"; section "Bootstrap phase 0: Poly/ML setup"; ML_file "ML/ml_init.ML"; ML_file "ML/ml_system.ML"; ML_file "System/distribution.ML"; ML_file "General/basics.ML"; ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; ML_file "Concurrent/synchronized.ML"; ML_file "Concurrent/counter.ML"; ML_file "ML/ml_heap.ML"; ML_file "ML/ml_profiling.ML"; ML_file "ML/ml_print_depth0.ML"; ML_file "ML/ml_pretty.ML"; ML_file "ML/ml_compiler0.ML"; section "Bootstrap phase 1: towards ML within position context"; subsection "Library of general tools"; ML_file "library.ML"; ML_file "General/print_mode.ML"; ML_file "General/alist.ML"; ML_file "General/table.ML"; ML_file "General/random.ML"; ML_file "General/value.ML"; ML_file "General/properties.ML"; ML_file "General/output.ML"; ML_file "PIDE/markup.ML"; ML_file "General/utf8.ML"; ML_file "General/scan.ML"; ML_file "General/source.ML"; ML_file "General/symbol.ML"; ML_file "General/position.ML"; ML_file "General/symbol_pos.ML"; ML_file "General/input.ML"; ML_file "General/comment.ML"; ML_file "General/antiquote.ML"; ML_file "ML/ml_lex.ML"; ML_file "ML/ml_compiler1.ML"; section "Bootstrap phase 2: towards ML within Isar context"; subsection "Library of general tools"; ML_file "General/integer.ML"; ML_file "General/stack.ML"; ML_file "General/queue.ML"; ML_file "General/heap.ML"; ML_file "General/same.ML"; ML_file "General/ord_list.ML"; ML_file "General/balanced_tree.ML"; ML_file "General/linear_set.ML"; ML_file "General/buffer.ML"; ML_file "General/pretty.ML"; ML_file "General/rat.ML"; ML_file "PIDE/xml.ML"; ML_file "General/path.ML"; ML_file "General/url.ML"; ML_file "System/bash_syntax.ML"; ML_file "General/file.ML"; ML_file "General/long_name.ML"; ML_file "General/binding.ML"; ML_file "General/socket_io.ML"; ML_file "General/seq.ML"; ML_file "General/timing.ML"; ML_file "General/sha1.ML"; ML_file "PIDE/byte_message.ML"; ML_file "PIDE/yxml.ML"; ML_file "PIDE/protocol_message.ML"; ML_file "PIDE/document_id.ML"; ML_file "General/change_table.ML"; ML_file "General/graph.ML"; ML_file "System/options.ML"; subsection "Fundamental structures"; ML_file "name.ML"; ML_file "term.ML"; ML_file "context.ML"; ML_file "config.ML"; ML_file "context_position.ML"; ML_file "soft_type_system.ML"; subsection "Concurrency within the ML runtime"; ML_file "ML/exn_properties.ML"; ML_file_no_debug "ML/exn_debugger.ML"; ML_file "ML/ml_statistics.ML"; ML_file "Concurrent/thread_data_virtual.ML"; ML_file "Concurrent/isabelle_thread.ML"; ML_file "Concurrent/single_assignment.ML"; ML_file "Concurrent/par_exn.ML"; ML_file "Concurrent/task_queue.ML"; ML_file "Concurrent/future.ML"; ML_file "Concurrent/event_timer.ML"; ML_file "Concurrent/timeout.ML"; ML_file "Concurrent/lazy.ML"; ML_file "Concurrent/par_list.ML"; ML_file "Concurrent/mailbox.ML"; ML_file "Concurrent/cache.ML"; ML_file "PIDE/active.ML"; ML_file "Thy/export.ML"; subsection "Inner syntax"; ML_file "Syntax/type_annotation.ML"; ML_file "Syntax/term_position.ML"; ML_file "Syntax/lexicon.ML"; ML_file "Syntax/ast.ML"; ML_file "Syntax/syntax_ext.ML"; ML_file "Syntax/parser.ML"; ML_file "Syntax/syntax_trans.ML"; ML_file "Syntax/mixfix.ML"; ML_file "Syntax/printer.ML"; ML_file "Syntax/syntax.ML"; subsection "Core of tactical proof system"; ML_file "term_ord.ML"; ML_file "term_subst.ML"; ML_file "General/completion.ML"; ML_file "General/name_space.ML"; ML_file "sorts.ML"; ML_file "type.ML"; ML_file "logic.ML"; ML_file "Syntax/simple_syntax.ML"; ML_file "net.ML"; ML_file "item_net.ML"; ML_file "envir.ML"; ML_file "consts.ML"; ML_file "term_xml.ML"; ML_file "primitive_defs.ML"; ML_file "sign.ML"; ML_file "defs.ML"; ML_file "term_sharing.ML"; ML_file "pattern.ML"; ML_file "unify.ML"; ML_file "theory.ML"; ML_file "proofterm.ML"; ML_file "thm.ML"; ML_file "more_pattern.ML"; ML_file "more_unify.ML"; ML_file "more_thm.ML"; ML_file "facts.ML"; ML_file "thm_name.ML"; ML_file "global_theory.ML"; ML_file "pure_thy.ML"; ML_file "drule.ML"; ML_file "morphism.ML"; ML_file "variable.ML"; ML_file "conv.ML"; ML_file "goal_display.ML"; ML_file "tactical.ML"; ML_file "search.ML"; ML_file "tactic.ML"; ML_file "raw_simplifier.ML"; ML_file "conjunction.ML"; ML_file "assumption.ML"; subsection "Isar -- Intelligible Semi-Automated Reasoning"; (*ML support and global execution*) ML_file "ML/ml_syntax.ML"; ML_file "ML/ml_env.ML"; ML_file "ML/ml_options.ML"; ML_file "ML/ml_print_depth.ML"; ML_file_no_debug "Isar/runtime.ML"; ML_file "PIDE/execution.ML"; ML_file "ML/ml_compiler.ML"; ML_file "skip_proof.ML"; ML_file "goal.ML"; (*outer syntax*) ML_file "Isar/keyword.ML"; ML_file "Isar/token.ML"; ML_file "Isar/parse.ML"; ML_file "Thy/document_source.ML"; ML_file "Thy/thy_header.ML"; ML_file "Thy/document_marker.ML"; (*proof context*) ML_file "Isar/object_logic.ML"; ML_file "Isar/rule_cases.ML"; ML_file "Isar/auto_bind.ML"; ML_file "type_infer.ML"; ML_file "Syntax/local_syntax.ML"; ML_file "Isar/proof_context.ML"; ML_file "type_infer_context.ML"; ML_file "Syntax/syntax_phases.ML"; ML_file "Isar/args.ML"; (*theory specifications*) ML_file "Isar/local_defs.ML"; ML_file "Isar/local_theory.ML"; ML_file "Isar/entity.ML"; ML_file "PIDE/command_span.ML"; ML_file "Thy/thy_element.ML"; ML_file "Thy/markdown.ML"; ML_file "Thy/html.ML"; ML_file "Thy/latex.ML"; (*ML with context and antiquotations*) ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; (*basic proof engine*) ML_file "par_tactical.ML"; ML_file "context_tactic.ML"; ML_file "Isar/proof_display.ML"; ML_file "Isar/attrib.ML"; ML_file "Isar/context_rules.ML"; ML_file "Isar/method.ML"; ML_file "Isar/proof.ML"; ML_file "Isar/element.ML"; ML_file "Isar/obtain.ML"; ML_file "Isar/subgoal.ML"; ML_file "Isar/calculation.ML"; (*local theories and targets*) ML_file "Isar/locale.ML"; ML_file "Isar/generic_target.ML"; ML_file "Isar/overloading.ML"; ML_file "axclass.ML"; ML_file "Isar/class.ML"; ML_file "Isar/named_target.ML"; ML_file "Isar/expression.ML"; ML_file "Isar/interpretation.ML"; ML_file "Isar/class_declaration.ML"; ML_file "Isar/bundle.ML"; ML_file "Isar/experiment.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; (*executable theory content*) ML_file "Isar/code.ML"; (*specifications*) ML_file "Isar/spec_rules.ML"; ML_file "Isar/specification.ML"; ML_file "Isar/parse_spec.ML"; ML_file "Isar/typedecl.ML"; (*toplevel transactions*) ML_file "Isar/proof_node.ML"; ML_file "Isar/toplevel.ML"; (*proof term operations*) ML_file "Proof/proof_rewrite_rules.ML"; ML_file "Proof/proof_syntax.ML"; ML_file "Proof/proof_checker.ML"; ML_file "Proof/extraction.ML"; (*Isabelle system*) ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; ML_file "ML/ml_antiquotations.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/thy_output.ML"; ML_file "Thy/document_antiquotations.ML"; ML_file "General/graph_display.ML"; ML_file "pure_syn.ML"; ML_file "PIDE/command.ML"; ML_file "PIDE/query_operation.ML"; ML_file "PIDE/resources.ML"; ML_file "Thy/present.ML"; ML_file "Thy/thy_info.ML"; ML_file "thm_deps.ML"; ML_file "Thy/export_theory.ML"; ML_file "Thy/sessions.ML"; ML_file "PIDE/session.ML"; ML_file "PIDE/document.ML"; (*theory and proof operations*) ML_file "Isar/isar_cmd.ML"; subsection "Isabelle/Isar system"; ML_file "System/command_line.ML"; ML_file "System/message_channel.ML"; ML_file "System/isabelle_process.ML"; ML_file "System/scala.ML"; +ML_file "System/scala_check.ML"; ML_file "Thy/bibtex.ML"; ML_file "PIDE/protocol.ML"; ML_file "General/output_primitives_virtual.ML"; subsection "Miscellaneous tools and packages for Pure Isabelle"; ML_file "ML/ml_pp.ML"; ML_file "ML/ml_thms.ML"; ML_file "ML/ml_file.ML"; ML_file "Tools/build.ML"; ML_file "Tools/named_thms.ML"; ML_file "Tools/print_operation.ML"; ML_file "Tools/rail.ML"; ML_file "Tools/rule_insts.ML"; ML_file "Tools/thy_deps.ML"; ML_file "Tools/class_deps.ML"; ML_file "Tools/find_theorems.ML"; ML_file "Tools/find_consts.ML"; ML_file "Tools/simplifier_trace.ML"; ML_file_no_debug "Tools/debugger.ML"; ML_file "Tools/named_theorems.ML"; ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" diff --git a/src/Pure/System/scala.ML b/src/Pure/System/scala.ML --- a/src/Pure/System/scala.ML +++ b/src/Pure/System/scala.ML @@ -1,83 +1,107 @@ (* Title: Pure/System/scala.ML Author: Makarius Support for Scala at runtime. *) signature SCALA = sig + val functions: unit -> string list + val check_function: Proof.context -> string * Position.T -> string val promise_function: string -> string -> string future val function: string -> string -> string exception Null - val check: string -> unit end; structure Scala: SCALA = struct (** invoke Scala functions from ML **) val _ = Session.protocol_handler "isabelle.Scala"; (* pending promises *) val new_id = string_of_int o Counter.make (); val promises = Synchronized.var "Scala.promises" (Symtab.empty: string future Symtab.table); (* invoke function *) fun promise_function name arg = let val _ = if Resources.is_pide () then () else raise Fail "PIDE session required"; val id = new_id (); fun abort () = Output.protocol_message (Markup.cancel_scala id) []; val promise = Future.promise_name "invoke_scala" abort : string future; val _ = Synchronized.change promises (Symtab.update (id, promise)); val _ = Output.protocol_message (Markup.invoke_scala name id) [XML.Text arg]; in promise end; fun function name arg = Future.join (promise_function name arg); (* fulfill *) exception Null; fun fulfill id tag res = let val result = (case tag of "0" => Exn.Exn Null | "1" => Exn.Res res | "2" => Exn.Exn (ERROR res) | "3" => Exn.Exn (Fail res) | "4" => Exn.Exn Exn.Interrupt | _ => raise Fail "Bad tag"); val promise = Synchronized.change_result promises (fn tab => (the (Symtab.lookup tab id), Symtab.delete id tab)); val _ = Future.fulfill_result promise result; in () end; val _ = Isabelle_Process.protocol_command "Scala.fulfill" (fn [id, tag, res] => fulfill id tag res handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); - -(** check source snippet **) +(* registered functions *) -fun check source = - let val errors = - function "scala_check" source - |> YXML.parse_body - |> let open XML.Decode in list string end - in if null errors then () else error (cat_lines errors) end; +fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); + +fun check_function ctxt (name, pos) = + let + val kind = Markup.scala_functionN; + val funs = functions (); + in + if member (op =) funs name then + (Context_Position.report ctxt pos (Markup.scala_function name); name) + else + let + val completion_report = + Completion.make_report (name, pos) + (fn completed => + filter completed funs + |> sort_strings + |> map (fn a => (a, (kind, a)))); + in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end + end; + +val _ = Theory.setup + (Thy_Output.antiquotation_verbatim_embedded \<^binding>\scala_function\ + (Scan.lift Parse.embedded_position) check_function #> + ML_Antiquotation.inline_embedded \<^binding>\scala_function\ + (Args.context -- Scan.lift Parse.embedded_position + >> (uncurry check_function #> ML_Syntax.print_string)) #> + ML_Antiquotation.value_embedded \<^binding>\scala\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => + let val name = check_function ctxt arg + in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); end; diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,200 +1,203 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle import java.io.{File => JFile, StringWriter, PrintWriter} import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} import scala.tools.nsc.interpreter.IMain object Scala { /** compiler **/ object Compiler { lazy val default_context: Context = context() def context( error: String => Unit = Exn.error, jar_dirs: List[JFile] = Nil): Context = { def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) val class_path = for { prop <- List("scala.boot.class.path", "java.class.path") path = System.getProperty(prop, "") if path != "\"\"" elem <- space_explode(JFile.pathSeparatorChar, path) } yield elem val settings = new GenericRunnerSettings(error) settings.classpath.value = (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) new Context(settings) } def default_print_writer: PrintWriter = new NewLinePrintWriter(new ConsoleWriter, true) class Context private [Compiler](val settings: GenericRunnerSettings) { override def toString: String = settings.toString def interpreter( print_writer: PrintWriter = default_print_writer, class_loader: ClassLoader = null): IMain = { new IMain(settings, print_writer) { override def parentClassLoader: ClassLoader = if (class_loader == null) super.parentClassLoader else class_loader } } def toplevel(source: String): List[String] = { val out = new StringWriter val interp = interpreter(new PrintWriter(out)) val rep = new interp.ReadEvalPrint val ok = interp.withLabel("\u0001") { rep.compile(source) } out.close val Error = """(?s)^\S* error: (.*)$""".r val errors = space_explode('\u0001', Library.strip_ansi_color(out.toString)). collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) if (!ok && errors.isEmpty) List("Error") else errors } def check(body: String): List[String] = { try { toplevel("package test\nobject Test { " + body + " }") } catch { case ERROR(msg) => List(msg) } } } } def check_yxml(body: String): String = { val errors = Compiler.default_context.check(body) locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) } } /** invoke Scala functions from ML **/ /* registered functions */ sealed case class Fun(name: String, apply: String => String) + { + override def toString: String = name + } lazy val functions: List[Fun] = Isabelle_System.services.collect { case c: Isabelle_Scala_Functions => c.functions.toList }.flatten /* invoke function */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } def function(name: String, arg: String): (Tag.Value, String) = functions.find(fun => fun.name == name) match { case Some(fun) => Exn.capture { fun.apply(arg) } match { case Exn.Res(null) => (Tag.NULL, "") case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "") case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) } case None => (Tag.FAIL, "Unknown Isabelle/Scala function: " + quote(name)) } } /* protocol handler */ class Scala extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(init_session: Session): Unit = synchronized { session = init_session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command("Scala.fulfill", id, tag.id.toString, res) futures -= id } } private def cancel(id: String, future: Future[Unit]) { future.cancel fulfill(id, Scala.Tag.INTERRUPT, "") } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Invoke_Scala(name, id) => futures += (id -> Future.fork { val (tag, result) = Scala.function(name, msg.text) fulfill(id, tag, result) }) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } val functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } /* registered functions */ class Isabelle_Scala_Functions(val functions: Scala.Fun*) extends Isabelle_System.Service class Functions extends Isabelle_Scala_Functions( Scala.Fun("echo", identity), Scala.Fun("scala_check", Scala.check_yxml), Scala.Fun("check_bibtex_database", Bibtex.check_database_yxml)) diff --git a/src/Pure/System/scala_check.ML b/src/Pure/System/scala_check.ML new file mode 100644 --- /dev/null +++ b/src/Pure/System/scala_check.ML @@ -0,0 +1,22 @@ +(* Title: Pure/System/scala_check.ML + Author: Makarius + +Semantic check of Scala sources. +*) + +signature SCALA_CHECK = +sig + val decl: string -> unit +end; + +structure Scala_Check: SCALA_CHECK = +struct + +fun decl source = + let val errors = + \<^scala>\scala_check\ source + |> YXML.parse_body + |> let open XML.Decode in list string end + in if null errors then () else error (cat_lines errors) end; + +end; diff --git a/src/Pure/Thy/bibtex.ML b/src/Pure/Thy/bibtex.ML --- a/src/Pure/Thy/bibtex.ML +++ b/src/Pure/Thy/bibtex.ML @@ -1,64 +1,64 @@ (* Title: Pure/Thy/bibtex.ML Author: Makarius BibTeX support. *) signature BIBTEX = sig val check_database: Position.T -> string -> (string * Position.T) list * (string * Position.T) list val check_database_output: Position.T -> string -> unit val cite_macro: string Config.T end; structure Bibtex: BIBTEX = struct (* check database *) type message = string * Position.T; fun check_database pos0 database = - Scala.function "check_bibtex_database" database + \<^scala>\check_bibtex_database\ database |> YXML.parse_body |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props pos0)); fun check_database_output pos0 database = let val (errors, warnings) = check_database pos0 database in errors |> List.app (fn (msg, pos) => Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n " ^ msg)); warnings |> List.app (fn (msg, pos) => warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg)) end; (* document antiquotations *) val cite_macro = Attrib.setup_config_string \<^binding>\cite_macro\ (K "cite"); val _ = Theory.setup (Document_Antiquotation.setup_option \<^binding>\cite_macro\ (Config.put cite_macro) #> Thy_Output.antiquotation_raw \<^binding>\cite\ (Scan.lift (Scan.option (Parse.verbatim || Parse.cartouche) -- Parse.and_list1 Args.name_position)) (fn ctxt => fn (opt, citations) => let val thy = Proof_Context.theory_of ctxt; val bibtex_entries = Present.get_bibtex_entries thy; val _ = if null bibtex_entries andalso Context.theory_name thy <> Context.PureN then () else citations |> List.app (fn (name, pos) => if member (op =) bibtex_entries name then () else error ("Unknown Bibtex entry " ^ quote name ^ Position.here pos)); val _ = Context_Position.reports ctxt (map (fn (name, pos) => (pos, Markup.citation name)) citations); val opt_arg = (case opt of NONE => "" | SOME s => "[" ^ s ^ "]"); val arg = "{" ^ space_implode "," (map #1 citations) ^ "}"; in Latex.string ("\\" ^ Config.get ctxt cite_macro ^ opt_arg ^ arg) end)); end;

code: 0x01d4ab group: letter \ code: 0x01d4ac group: letter \ code: 0x00211b group: letter \ code: 0x01d4ae group: letter \ code: 0x01d4af group: letter \ code: 0x01d4b0 group: letter \ code: 0x01d4b1 group: letter \ code: 0x01d4b2 group: letter \ code: 0x01d4b3 group: letter \ code: 0x01d4b4 group: letter \ code: 0x01d4b5 group: letter \ code: 0x01d5ba group: letter \ code: 0x01d5bb group: letter \ code: 0x01d5bc group: letter \ code: 0x01d5bd group: letter \ code: 0x01d5be group: letter \ code: 0x01d5bf group: letter \ code: 0x01d5c0 group: letter \ code: 0x01d5c1 group: letter \ code: 0x01d5c2 group: letter \ code: 0x01d5c3 group: letter \ code: 0x01d5c4 group: letter \ code: 0x01d5c5 group: letter \ code: 0x01d5c6 group: letter \ code: 0x01d5c7 group: letter \ code: 0x01d5c8 group: letter \