# HG changeset patch # User wenzelm # Date 1310149629 -7200 # Node ID 608d1b451f678c632fe0c48a4d96e88422df5540 # Parent 7270ae921cf28be0add6bd7f68d97c69bb0940b2 less stateful outer_syntax; diff -r 7270ae921cf2 -r 608d1b451f67 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Jul 08 17:04:38 2011 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Fri Jul 08 20:27:09 2011 +0200 @@ -9,13 +9,16 @@ signature OUTER_SYNTAX = sig + type outer_syntax + val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax val command: string -> string -> Keyword.T -> (Toplevel.transition -> Toplevel.transition) parser -> unit val markup_command: Thy_Output.markup -> string -> string -> Keyword.T -> (Toplevel.transition -> Toplevel.transition) parser -> unit val improper_command: string -> string -> Keyword.T -> (Toplevel.transition -> Toplevel.transition) parser -> unit - val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit + val internal_command: string -> + (Toplevel.transition -> Toplevel.transition) parser -> unit val local_theory': string -> string -> Keyword.T -> (bool -> local_theory -> local_theory) parser -> unit val local_theory: string -> string -> Keyword.T -> @@ -77,40 +80,56 @@ end; +(* type outer_syntax *) + +datatype outer_syntax = Outer_Syntax of + {commands: command Symtab.table, + markups: (string * Thy_Output.markup) list}; + +fun make_outer_syntax commands markups = + Outer_Syntax {commands = commands, markups = markups}; + +val empty_outer_syntax = make_outer_syntax Symtab.empty []; + + +fun map_commands f (Outer_Syntax {commands, ...}) = + let + val commands' = f commands; + val markups' = + Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I) + commands' []; + in make_outer_syntax commands' markups' end; + +fun dest_commands (Outer_Syntax {commands, ...}) = + commands |> Symtab.dest |> sort_wrt #1 + |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only)); + +fun lookup_commands (Outer_Syntax {commands, ...}) = Symtab.lookup commands; + +fun is_markup (Outer_Syntax {markups, ...}) kind name = + AList.lookup (op =) markups name = SOME kind; + + (** global outer syntax **) local -val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table); -val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list); +(*synchronized wrt. Keywords*) +val global_outer_syntax = Unsynchronized.ref empty_outer_syntax; -fun change_commands f = CRITICAL (fn () => - (Unsynchronized.change global_commands f; - global_markups := - Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I) - (! global_commands) [])); +fun add_command name kind cmd = CRITICAL (fn () => + (Keyword.command name kind; + Unsynchronized.change global_outer_syntax (map_commands (fn commands => + (if not (Symtab.defined commands name) then () + else warning ("Redefining outer syntax command " ^ quote name); + Symtab.update (name, cmd) commands))))); in -(* access current syntax *) - -fun get_commands () = ! global_commands; -fun get_markups () = ! global_markups; - -fun get_command () = Symtab.lookup (get_commands ()); -fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), get_command ())); +fun get_syntax () = CRITICAL (fn () => (Keyword.get_lexicons (), ! global_outer_syntax)); -fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind; - - -(* augment syntax *) - -fun add_command name kind cmd = CRITICAL (fn () => - (Keyword.command name kind; - if not (Symtab.defined (get_commands ()) name) then () - else warning ("Redefining outer syntax command " ^ quote name); - change_commands (Symtab.update (name, cmd)))); +fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax); fun command name comment kind parse = add_command name kind (make_command comment NONE false parse); @@ -121,11 +140,11 @@ fun improper_command name comment kind parse = add_command name kind (make_command comment NONE true parse); -end; - fun internal_command name parse = command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr)); +end; + (* local_theory commands *) @@ -141,17 +160,15 @@ (* inspect syntax *) -fun dest_commands () = - get_commands () |> Symtab.dest |> sort_wrt #1 - |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only)); - fun print_outer_syntax () = let + val (keywords, outer_syntax) = + CRITICAL (fn () => (Keyword.dest_keywords (), #2 (get_syntax ()))); fun pretty_cmd (name, comment, _) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; - val (int_cmds, cmds) = List.partition #3 (dest_commands ()); + val (int_cmds, cmds) = List.partition #3 (dest_commands outer_syntax); in - [Pretty.strs ("syntax keywords:" :: map quote (Keyword.dest_keywords ())), + [Pretty.strs ("syntax keywords:" :: map quote keywords), Pretty.big_list "commands:" (map pretty_cmd cmds), Pretty.big_list "interactive-only commands:" (map pretty_cmd int_cmds)] |> Pretty.chunks |> Pretty.writeln @@ -195,7 +212,7 @@ Source.of_string str |> Symbol.source |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos - |> toplevel_source false NONE get_command + |> toplevel_source false NONE lookup_commands_dynamic |> Source.exhaust; @@ -226,15 +243,16 @@ Source.tty in_stream |> Symbol.source |> Token.source {do_recover = SOME true} Keyword.get_lexicons Position.none - |> toplevel_source term (SOME true) get_command; + |> toplevel_source term (SOME true) lookup_commands_dynamic; (* prepare toplevel commands -- fail-safe *) val not_singleton = "Exactly one command expected"; -fun prepare_span commands span = +fun prepare_span outer_syntax span = let + val commands = lookup_commands outer_syntax; val range_pos = Position.set_range (Thy_Syntax.span_range span); val toks = Thy_Syntax.span_content span; val _ = List.app Thy_Syntax.report_token toks; @@ -249,19 +267,19 @@ handle ERROR msg => (Toplevel.malformed range_pos msg, true) end; -fun prepare_element commands init {head, proof, proper_proof} = +fun prepare_element outer_syntax init {head, proof, proper_proof} = let - val (tr, proper_head) = prepare_span commands head |>> Toplevel.modify_init init; - val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1; + val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init; + val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1; in if proper_head andalso proper_proof then [(tr, proof_trs)] else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs) end; fun prepare_command pos str = - let val (lexs, commands) = get_syntax () in + let val (lexs, outer_syntax) = get_syntax () in (case Thy_Syntax.parse_spans lexs pos str of - [span] => #1 (prepare_span commands span) + [span] => #1 (prepare_span outer_syntax span) | _ => Toplevel.malformed pos not_singleton) end; @@ -270,7 +288,7 @@ fun load_thy name init pos text = let - val (lexs, commands) = get_syntax (); + val (lexs, outer_syntax) = get_syntax (); val time = ! Toplevel.timing; val _ = Present.init_theory name; @@ -278,8 +296,10 @@ val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text)); val spans = Source.exhaust (Thy_Syntax.span_source toks); val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *) - val elements = Source.exhaust (Thy_Syntax.element_source (Source.of_list spans)) - |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element commands init) |> flat; + val elements = + Source.exhaust (Thy_Syntax.element_source (Source.of_list spans)) + |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element outer_syntax init) + |> flat; val _ = Present.theory_source name (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); @@ -292,7 +312,7 @@ singleton (Future.cond_forks {name = "Outer_Syntax.present:" ^ name, group = NONE, deps = map Future.task_of results, pri = 0}) (fn () => - Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup + Thy_Output.present_thy (#1 lexs) Keyword.command_tags (is_markup outer_syntax) (maps Future.join results) toks |> Buffer.content |> Present.theory_output name);