equal
deleted
inserted
replaced
56 Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args; |
56 Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args; |
57 |
57 |
58 val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _"; |
58 val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _"; |
59 |
59 |
60 fun scala_name name = |
60 fun scala_name name = |
61 let val latex = Latex.string (Latex.output_ascii_breakable "." name) |
61 Latex.string (Latex.output_ascii_breakable "." name) |
62 in Latex.enclose_block "\\isatt{" "}" [latex] end; |
62 |> Latex.enclose_text "\\isatt{" "}"; |
63 |
63 |
64 in |
64 in |
65 |
65 |
66 val _ = |
66 val _ = |
67 Theory.setup |
67 Theory.setup |