moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
authorwenzelm
Tue Aug 16 13:42:42 2005 +0200 (2005-08-16)
changeset 17071f753d6dd9bd0
parent 17070 3b29a01417f8
child 17072 501c28052aea
moved structure Keyword to OuterKeyword (Isar/outer_keyword.ML);
support for tagged commands;
tuned theory presentation interface;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 16 13:42:41 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 16 13:42:42 2005 +0200
     1.3 @@ -19,39 +19,13 @@
     1.4  signature OUTER_SYNTAX =
     1.5  sig
     1.6    include BASIC_OUTER_SYNTAX
     1.7 -  structure Keyword:
     1.8 -    sig
     1.9 -      val control: string
    1.10 -      val diag: string
    1.11 -      val thy_begin: string
    1.12 -      val thy_switch: string
    1.13 -      val thy_end: string
    1.14 -      val thy_heading: string
    1.15 -      val thy_decl: string
    1.16 -      val thy_script: string
    1.17 -      val thy_goal: string
    1.18 -      val qed: string
    1.19 -      val qed_block: string
    1.20 -      val qed_global: string
    1.21 -      val prf_heading: string
    1.22 -      val prf_goal: string
    1.23 -      val prf_block: string
    1.24 -      val prf_open: string
    1.25 -      val prf_close: string
    1.26 -      val prf_chain: string
    1.27 -      val prf_decl: string
    1.28 -      val prf_asm: string
    1.29 -      val prf_asm_goal: string
    1.30 -      val prf_script: string
    1.31 -      val kinds: string list
    1.32 -    end
    1.33    type token
    1.34    type parser
    1.35 -  val command: string -> string -> string ->
    1.36 +  val command: string -> string -> OuterKeyword.T ->
    1.37      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.38 -  val markup_command: IsarOutput.markup -> string -> string -> string ->
    1.39 +  val markup_command: IsarOutput.markup -> string -> string -> OuterKeyword.T ->
    1.40      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.41 -  val improper_command: string -> string -> string ->
    1.42 +  val improper_command: string -> string -> OuterKeyword.T ->
    1.43      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.44    val is_keyword: string -> bool
    1.45    val dest_keywords: unit -> string list
    1.46 @@ -77,46 +51,13 @@
    1.47  
    1.48  (** outer syntax **)
    1.49  
    1.50 -(* command keyword classification *)
    1.51 -
    1.52 -structure Keyword =
    1.53 -struct
    1.54 -  val control = "control";
    1.55 -  val diag = "diag";
    1.56 -  val thy_begin = "theory-begin";
    1.57 -  val thy_switch = "theory-switch";
    1.58 -  val thy_end = "theory-end";
    1.59 -  val thy_heading = "theory-heading";
    1.60 -  val thy_decl = "theory-decl";
    1.61 -  val thy_script = "theory-script";
    1.62 -  val thy_goal = "theory-goal";
    1.63 -  val qed = "qed";
    1.64 -  val qed_block = "qed-block";
    1.65 -  val qed_global = "qed-global";
    1.66 -  val prf_heading = "proof-heading";
    1.67 -  val prf_goal = "proof-goal";
    1.68 -  val prf_block = "proof-block";
    1.69 -  val prf_open = "proof-open";
    1.70 -  val prf_close = "proof-close";
    1.71 -  val prf_chain = "proof-chain";
    1.72 -  val prf_decl = "proof-decl";
    1.73 -  val prf_asm = "proof-asm";
    1.74 -  val prf_asm_goal = "proof-asm-goal";
    1.75 -  val prf_script = "proof-script";
    1.76 -
    1.77 -  val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
    1.78 -    thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    1.79 -    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.80 -end;
    1.81 -
    1.82 -
    1.83  (* parsers *)
    1.84  
    1.85  type token = T.token;
    1.86  type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    1.87  
    1.88  datatype parser =
    1.89 -  Parser of string * (string * string * IsarOutput.markup option) * bool * parser_fn;
    1.90 +  Parser of string * (string * OuterKeyword.T * IsarOutput.markup option) * bool * parser_fn;
    1.91  
    1.92  fun parser int_only markup name comment kind parse =
    1.93    Parser (name, (comment, kind, markup), int_only, parse);
    1.94 @@ -132,10 +73,10 @@
    1.95  fun trace false parse = parse
    1.96    | trace true parse = Scan.trace parse >> (fn (f, toks) => f o Toplevel.source toks);
    1.97  
    1.98 -fun body cmd trc (name, _) =
    1.99 +fun body cmd do_trace (name, _) =
   1.100    (case cmd name of
   1.101      SOME (int_only, parse) =>
   1.102 -      P.!!! (Scan.prompt (name ^ "# ") (trace trc parse >> pair int_only))
   1.103 +      P.!!! (Scan.prompt (name ^ "# ") (trace do_trace parse >> pair int_only))
   1.104    | NONE => sys_error ("no parser for outer syntax command " ^ quote name));
   1.105  
   1.106  in
   1.107 @@ -143,7 +84,7 @@
   1.108  fun command do_terminate do_trace cmd =
   1.109    P.semicolon >> K NONE ||
   1.110    P.sync >> K NONE ||
   1.111 -  (P.position P.command :-- body cmd do_trace) --| terminate do_terminate
   1.112 +  ((P.position P.command --| P.tags) :-- body cmd do_trace) --| terminate do_terminate
   1.113      >> (fn ((name, pos), (int_only, f)) =>
   1.114        SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
   1.115          Toplevel.interactive int_only |> f));
   1.116 @@ -158,7 +99,7 @@
   1.117  
   1.118  val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
   1.119  val global_parsers =
   1.120 -  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * IsarOutput.markup option)
   1.121 +  ref (Symtab.empty: (((string * OuterKeyword.T) * (bool * parser_fn)) * IsarOutput.markup option)
   1.122      Symtab.table);
   1.123  val global_markups = ref ([]: (string * IsarOutput.markup) list);
   1.124  
   1.125 @@ -169,10 +110,9 @@
   1.126      | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
   1.127    end;
   1.128  
   1.129 -fun get_markup (ms, (name, (_, SOME m))) = (name, m) :: ms
   1.130 -  | get_markup (ms, _) = ms;
   1.131 +fun make_markups () = global_markups :=
   1.132 +  Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) [];
   1.133  
   1.134 -fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
   1.135  fun change_parsers f = (Library.change global_parsers f; make_markups ());
   1.136  
   1.137  in
   1.138 @@ -185,11 +125,14 @@
   1.139  
   1.140  fun get_lexicons () = ! global_lexicons;
   1.141  fun get_parsers () = ! global_parsers;
   1.142 -fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (! global_parsers);
   1.143 +fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (get_parsers ());
   1.144  
   1.145 -fun is_markup kind name =
   1.146 -  (case assoc (! global_markups, name) of SOME k => k = kind | NONE => false);
   1.147 -fun markup kind = Scan.one (T.is_kind T.Command andf is_markup kind o T.val_of);
   1.148 +fun command_tags name =
   1.149 +  (case Symtab.lookup (get_parsers (), name) of
   1.150 +    SOME (((_, k), _), _) => OuterKeyword.tags_of k
   1.151 +  | NONE => []);
   1.152 +
   1.153 +fun is_markup kind name = (assoc_string (! global_markups, name) = SOME kind);
   1.154  
   1.155  
   1.156  (* augment syntax *)
   1.157 @@ -197,13 +140,13 @@
   1.158  fun add_keywords keywords = change_lexicons (apfst (fn lex =>
   1.159    (Scan.extend_lexicon lex (map Symbol.explode keywords))));
   1.160  
   1.161 -fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) =
   1.162 +fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
   1.163   (if not (Symtab.defined tab name) then ()
   1.164    else warning ("Redefined outer syntax command " ^ quote name);
   1.165    Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
   1.166  
   1.167  fun add_parsers parsers =
   1.168 -  (change_parsers (fn tab => Library.foldl add_parser (tab, parsers));
   1.169 +  (change_parsers (fold add_parser parsers);
   1.170      change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
   1.171        (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
   1.172  
   1.173 @@ -217,7 +160,8 @@
   1.174  
   1.175  fun dest_parsers () =
   1.176    get_parsers () |> Symtab.dest |> sort_wrt #1
   1.177 -  |> map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only));
   1.178 +  |> map (fn (name, (((cmt, kind), (int_only, _)), _)) =>
   1.179 +    (name, cmt, OuterKeyword.kind_of kind, int_only));
   1.180  
   1.181  fun print_outer_syntax () =
   1.182    let
   1.183 @@ -239,7 +183,7 @@
   1.184  
   1.185  (* basic sources *)
   1.186  
   1.187 -fun toplevel_source term trc do_recover cmd src =
   1.188 +fun toplevel_source term do_trace do_recover cmd src =
   1.189    let
   1.190      val no_terminator =
   1.191        Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
   1.192 @@ -251,7 +195,7 @@
   1.193        (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
   1.194        (if do_recover then SOME recover else NONE)
   1.195      |> Source.mapfilter I
   1.196 -    |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term trc (cmd ())) xs))
   1.197 +    |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
   1.198        (if do_recover then SOME recover else NONE)
   1.199      |> Source.mapfilter I
   1.200    end;
   1.201 @@ -325,11 +269,6 @@
   1.202      else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
   1.203    end;
   1.204  
   1.205 -fun parse_thy src =
   1.206 -  src
   1.207 -  |> toplevel_source false false false (K (get_parser ()))
   1.208 -  |> Source.exhaust;
   1.209 -
   1.210  fun run_thy name path =
   1.211    let
   1.212      val pos = Path.position path;
   1.213 @@ -347,10 +286,15 @@
   1.214            |> Symbol.source false
   1.215            |> T.source false (K (get_lexicons ())) pos
   1.216            |> Source.exhausted;
   1.217 -        val out = Toplevel.excursion_result
   1.218 -          (IsarOutput.parse_thy markup (#1 (get_lexicons ()))
   1.219 -            (parse_thy tok_src) tok_src);
   1.220 -      in Present.theory_output name (Buffer.content out) end
   1.221 +        val trs =
   1.222 +          tok_src
   1.223 +          |> toplevel_source false false false (K (get_parser ()))
   1.224 +          |> Source.exhaust;
   1.225 +      in
   1.226 +        IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs tok_src
   1.227 +        |> Buffer.content
   1.228 +        |> Present.theory_output name
   1.229 +      end
   1.230    end;
   1.231  
   1.232  in