verbatim markup tokens;
authorwenzelm
Thu Oct 07 17:20:58 1999 +0200 (1999-10-07)
changeset 778957d20133224e
parent 7788 825b8b1ad136
child 7790 2fd4d53acc0a
verbatim markup tokens;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 07 17:20:19 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 07 17:20:58 1999 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  val textP = OuterSyntax.markup_command "text" "formal comment (theory)" K.thy_decl
     1.5    (P.comment >> (Toplevel.theory o IsarThy.add_text));
     1.6  
     1.7 -val verbatimP = OuterSyntax.markup_command "verbatim" "verbatim document preparation text"
     1.8 +val verbatimP = OuterSyntax.verbatim_command "verbatim" "verbatim document preparation text"
     1.9    K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_verbatim));
    1.10  
    1.11  
    1.12 @@ -74,7 +74,7 @@
    1.13  val txtP = OuterSyntax.markup_command "txt" "formal comment (proof)" K.prf_decl
    1.14    (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt)));
    1.15  
    1.16 -val verbP = OuterSyntax.markup_command "verb" "verbatim document preparation text (proof)"
    1.17 +val verbP = OuterSyntax.verbatim_command "verb" "verbatim document preparation text (proof)"
    1.18    K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_verb)));
    1.19  
    1.20  
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 17:20:19 1999 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Oct 07 17:20:58 1999 +0200
     2.3 @@ -44,6 +44,8 @@
     2.4      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     2.5    val markup_command: string -> string -> string ->
     2.6      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     2.7 +  val verbatim_command: string -> string -> string ->
     2.8 +    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     2.9    val improper_command: string -> string -> string ->
    2.10      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    2.11    val dest_keywords: unit -> string list
    2.12 @@ -100,7 +102,7 @@
    2.13  type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    2.14  
    2.15  datatype parser =
    2.16 -  Parser of string * (string * string * bool) * bool * parser_fn;
    2.17 +  Parser of string * (string * string * bool option) * bool * parser_fn;
    2.18  
    2.19  fun parser int_only markup name comment kind parse =
    2.20    Parser (name, (comment, kind, markup), int_only, parse);
    2.21 @@ -138,8 +140,8 @@
    2.22  
    2.23  val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
    2.24  val global_parsers =
    2.25 -  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool) Symtab.table);
    2.26 -val global_markups = ref ([]: string list);
    2.27 +  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * bool option) Symtab.table);
    2.28 +val global_markups = ref ([]: (string * bool) list);
    2.29  
    2.30  fun change_lexicons f =
    2.31    let val lexs = f (! global_lexicons) in
    2.32 @@ -148,8 +150,8 @@
    2.33      | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
    2.34    end;
    2.35  
    2.36 -fun get_markup (names, (name, (_, true))) = name :: names
    2.37 -  | get_markup (names, _) = names;
    2.38 +fun get_markup (ms, (name, (_, Some m))) = (name, m) :: ms
    2.39 +  | get_markup (ms, _) = ms;
    2.40  
    2.41  fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
    2.42  fun change_parsers f = (global_parsers := f (! global_parsers); make_markups ());
    2.43 @@ -165,7 +167,10 @@
    2.44  fun get_lexicons () = ! global_lexicons;
    2.45  fun get_parsers () = ! global_parsers;
    2.46  fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
    2.47 -fun is_markup name = name mem_string ! global_markups;
    2.48 +
    2.49 +fun lookup_markup name = assoc (! global_markups, name);
    2.50 +fun is_markup name = if_none (lookup_markup name) false;
    2.51 +fun is_verbatim name = if_none (apsome not (lookup_markup name)) false;
    2.52  
    2.53  
    2.54  (* augment syntax *)
    2.55 @@ -335,11 +340,14 @@
    2.56  
    2.57  val improper = Scan.any (not o T.is_proper);
    2.58  val markup = Scan.one (T.is_kind T.Command andf is_markup o T.val_of) >> T.val_of;
    2.59 +val verbatim = Scan.one (T.is_kind T.Command andf is_verbatim o T.val_of);
    2.60  
    2.61  val present_token =
    2.62    improper |-- markup -- (improper |-- P.text --| (improper -- Scan.option semicolon -- improper))
    2.63      >> Present.markup_token ||
    2.64    (P.$$$ "--" >> K "cmt") -- (improper |-- P.text) >> Present.markup_token ||
    2.65 +  (improper -- verbatim -- improper) |-- P.text --| (improper -- Scan.option semicolon -- improper)
    2.66 +    >> Present.verbatim_token ||
    2.67    Scan.one T.not_eof >> Present.basic_token;
    2.68  
    2.69  in
    2.70 @@ -446,9 +454,10 @@
    2.71  
    2.72  
    2.73  (*final declarations of this structure!*)
    2.74 -val command = parser false false;
    2.75 -val markup_command = parser false true;
    2.76 -val improper_command = parser true false;
    2.77 +val command = parser false None;
    2.78 +val markup_command = parser false (Some true);
    2.79 +val verbatim_command = parser false (Some false);
    2.80 +val improper_command = parser true None;
    2.81  
    2.82  
    2.83  end;
     3.1 --- a/src/Pure/Thy/latex.ML	Thu Oct 07 17:20:19 1999 +0200
     3.2 +++ b/src/Pure/Thy/latex.ML	Thu Oct 07 17:20:58 1999 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  
     3.5  signature LATEX =
     3.6  sig
     3.7 -  datatype token = Basic of OuterLex.token | Markup of string * string
     3.8 +  datatype token = Basic of OuterLex.token | Markup of string * string | Verbatim of string
     3.9    val token_source: token list -> string
    3.10    val theory_entry: string -> string
    3.11  end;
    3.12 @@ -51,7 +51,7 @@
    3.13  
    3.14  structure T = OuterLex;
    3.15  
    3.16 -datatype token = Basic of T.token | Markup of string * string;
    3.17 +datatype token = Basic of T.token | Markup of string * string | Verbatim of string;
    3.18  
    3.19  
    3.20  val invisible_token = T.keyword_with (equal ";") orf T.is_kind T.Comment;
    3.21 @@ -69,7 +69,8 @@
    3.22          else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
    3.23          else output_sym s
    3.24        end
    3.25 -  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n";
    3.26 +  | output_tok (Markup (cmd, arg)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks arg ^ "}\n"
    3.27 +  | output_tok (Verbatim txt) = "\n" ^ txt ^ "\n";
    3.28  
    3.29  
    3.30  val output_tokens = implode o map output_tok;
     4.1 --- a/src/Pure/Thy/present.ML	Thu Oct 07 17:20:19 1999 +0200
     4.2 +++ b/src/Pure/Thy/present.ML	Thu Oct 07 17:20:58 1999 +0200
     4.3 @@ -20,6 +20,7 @@
     4.4    type token
     4.5    val basic_token: OuterLex.token -> token
     4.6    val markup_token: string * string -> token
     4.7 +  val verbatim_token: string -> token
     4.8    val token_source: string -> (unit -> token list) -> unit
     4.9    val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
    4.10    val result: string -> string -> thm -> unit
    4.11 @@ -355,6 +356,7 @@
    4.12  type token = Latex.token;
    4.13  val basic_token = Latex.Basic;
    4.14  val markup_token = Latex.Markup;
    4.15 +val verbatim_token = Latex.Verbatim;
    4.16  
    4.17  fun token_source name mk_toks =
    4.18    with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));