# HG changeset patch # User wenzelm # Date 1415285224 -3600 # Node ID cb9b69cca999e53d365449978e85df26f272b86a # Parent 1f500b18c4c6841aca732b34f5e1078318400e73 more explicit Keyword.keywords; diff -r 1f500b18c4c6 -r cb9b69cca999 src/Doc/antiquote_setup.ML --- a/src/Doc/antiquote_setup.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Doc/antiquote_setup.ML Thu Nov 06 15:47:04 2014 +0100 @@ -195,14 +195,16 @@ Keyword.is_keyword (Keyword.get_keywords ()) name; fun check_command ctxt (name, pos) = - is_some (Keyword.command_keyword name) andalso - let - val markup = - Outer_Syntax.scan (Keyword.get_keywords ()) Position.none name - |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) - |> map (snd o fst); - val _ = Context_Position.reports ctxt (map (pair pos) markup); - in true end; + let val keywords = Keyword.get_keywords () in + is_some (Keyword.command_keyword keywords name) andalso + let + val markup = + Outer_Syntax.scan keywords Position.none name + |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) + |> map (snd o fst); + val _ = Context_Position.reports ctxt (map (pair pos) markup); + in true end + end; fun check_system_option ctxt (name, pos) = (Context_Position.report ctxt pos (Options.default_markup (name, pos)); true) diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/Isar/keyword.ML Thu Nov 06 15:47:04 2014 +0100 @@ -41,25 +41,25 @@ val empty_keywords: keywords val merge_keywords: keywords * keywords -> keywords val add_keywords: string * T option -> keywords -> keywords + val is_keyword: keywords -> string -> bool + val command_keyword: keywords -> string -> T option + val command_files: keywords -> string -> Path.T -> Path.T list + val command_tags: keywords -> string -> string list + val is_diag: keywords -> string -> bool + val is_heading: keywords -> string -> bool + val is_theory_begin: keywords -> string -> bool + val is_theory_load: keywords -> string -> bool + val is_theory: keywords -> string -> bool + val is_theory_body: keywords -> string -> bool + val is_proof: keywords -> string -> bool + val is_proof_body: keywords -> string -> bool + val is_theory_goal: keywords -> string -> bool + val is_proof_goal: keywords -> string -> bool + val is_qed: keywords -> string -> bool + val is_qed_global: keywords -> string -> bool + val is_printed: keywords -> string -> bool val define: string * T option -> unit val get_keywords: unit -> keywords - val is_keyword: keywords -> string -> bool - val command_keyword: string -> T option - val command_files: string -> Path.T -> Path.T list - val command_tags: string -> string list - val is_diag: string -> bool - val is_heading: string -> bool - val is_theory_begin: string -> bool - val is_theory_load: string -> bool - val is_theory: string -> bool - val is_theory_body: string -> bool - val is_proof: string -> bool - val is_proof_body: string -> bool - val is_theory_goal: string -> bool - val is_proof_goal: string -> bool - val is_qed: string -> bool - val is_qed_global: string -> bool - val is_printed: string -> bool end; structure Keyword: KEYWORD = @@ -134,7 +134,6 @@ fun minor_keywords (Keywords {minor, ...}) = minor; fun major_keywords (Keywords {major, ...}) = major; -fun commands (Keywords {commands, ...}) = commands; fun make_keywords (minor, major, commands) = Keywords {minor = minor, major = major, commands = commands}; @@ -172,18 +171,6 @@ in (minor, major', commands') end)); -(* global state *) - -local val global_keywords = Unsynchronized.ref empty_keywords in - -fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl)); -fun get_keywords () = ! global_keywords; - -end; - -fun get_commands () = commands (get_keywords ()); - - (* lookup *) fun is_keyword keywords s = @@ -193,18 +180,18 @@ val syms = Symbol.explode s; in Scan.is_literal minor syms orelse Scan.is_literal major syms end; -fun command_keyword name = Symtab.lookup (get_commands ()) name; +fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands; -fun command_files name path = - (case command_keyword name of +fun command_files keywords name path = + (case command_keyword keywords name of NONE => [] | SOME (Keyword {kind, files, ...}) => if kind <> kind_of thy_load then [] else if null files then [path] else map (fn ext => Path.ext ext path) files); -fun command_tags name = - (case command_keyword name of +fun command_tags keywords name = + (case command_keyword keywords name of SOME (Keyword {tags, ...}) => tags | NONE => []); @@ -212,12 +199,13 @@ (* command categories *) fun command_category ks = - let val tab = Symtab.make_set (map kind_of ks) in - fn name => - (case command_keyword name of + let + val tab = Symtab.make_set (map kind_of ks); + fun pred keywords name = + (case command_keyword keywords name of NONE => false - | SOME k => Symtab.defined tab (kind_of k)) - end; + | SOME k => Symtab.defined tab (kind_of k)); + in pred end; val is_diag = command_category [diag]; @@ -246,7 +234,18 @@ val is_qed = command_category [qed, qed_script, qed_block]; val is_qed_global = command_category [qed_global]; -val is_printed = is_theory_goal orf is_proof; +fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; + + + +(** global state **) + +local val global_keywords = Unsynchronized.ref empty_keywords in + +fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl)); +fun get_keywords () = ! global_keywords; end; +end; + diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/Isar/toplevel.ML Thu Nov 06 15:47:04 2014 +0100 @@ -88,7 +88,7 @@ val reset_proof: state -> state option type result val join_results: result -> (transition * state) list - val element_result: transition Thy_Syntax.element -> state -> result * state + val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state end; structure Toplevel: TOPLEVEL = @@ -681,10 +681,10 @@ NONE => Goal.future_enabled 2 | SOME t => Goal.future_enabled_timing t))); -fun atom_result tr st = +fun atom_result keywords tr st = let val st' = - if Goal.future_enabled 1 andalso Keyword.is_diag (name_of tr) then + if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then (Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = priority (timing_estimate true (Thy_Syntax.atom tr))} @@ -694,10 +694,10 @@ in -fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st - | element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st = +fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st + | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st = let - val (head_result, st') = atom_result head_tr st; + val (head_result, st') = atom_result keywords head_tr st; val (body_elems, end_tr) = element_rest; val estimate = timing_estimate false elem; in @@ -705,7 +705,7 @@ then let val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr]; - val (proof_results, st'') = fold_map atom_result proof_trs st'; + val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; in (Result_List (head_result :: proof_results), st'') end else let @@ -721,7 +721,7 @@ val prf' = Proof_Node.apply (K state) prf; val (result, result_state) = State (SOME (Proof (prf', (finish, orig_gthy))), prev) - |> fold_map element_result body_elems ||> command end_tr; + |> fold_map (element_result keywords) body_elems ||> command end_tr; in (Result_List result, presentation_context_of result_state) end)) #> (fn (res, state') => state' |> put_result (Result_Future res)); diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/PIDE/command.ML Thu Nov 06 15:47:04 2014 +0100 @@ -8,19 +8,21 @@ sig type blob = (string * (SHA1.digest * string list) option) Exn.result val read_file: Path.T -> Position.T -> Path.T -> Token.file - val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition + val read: Keyword.keywords -> Path.T-> (unit -> theory) -> blob list -> Token.T list -> + Toplevel.transition type eval val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool val eval_result_state: eval -> Toplevel.state - val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval + val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> blob list -> Token.T list -> + eval -> eval type print - val print: bool -> (string * string list) list -> string -> + val print: bool -> (string * string list) list -> Keyword.keywords -> string -> eval -> print list -> print list option type print_fn = Toplevel.transition -> Toplevel.state -> unit type print_function = - {command_name: string, args: string list, exec_id: Document_ID.exec} -> + {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option val print_function: string -> print_function -> unit val no_print_function: string -> unit @@ -120,10 +122,10 @@ | SOME exec_id => Position.put_id exec_id); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end -fun resolve_files master_dir blobs toks = +fun resolve_files keywords master_dir blobs toks = (case Outer_Syntax.parse_spans toks of [span] => span - |> Command_Span.resolve_files (fn cmd => fn (path, pos) => + |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) => let fun make_file src_path (Exn.Res (file_node, NONE)) = Exn.interruptible_capture (fn () => @@ -132,7 +134,7 @@ (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)]; Exn.Res (blob_file src_path lines digest file_node)) | make_file _ (Exn.Exn e) = Exn.Exn e; - val src_paths = Keyword.command_files cmd path; + val src_paths = Keyword.command_files keywords cmd path; in if null blobs then map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) @@ -145,7 +147,7 @@ in -fun read init master_dir blobs span = +fun read keywords master_dir init blobs span = let val syntax = #2 (Outer_Syntax.get_syntax ()); val command_reports = Outer_Syntax.command_reports syntax; @@ -161,7 +163,7 @@ in if is_malformed then Toplevel.malformed pos "Malformed command syntax" else - (case Outer_Syntax.read_spans syntax (resolve_files master_dir blobs span) of + (case Outer_Syntax.read_spans syntax (resolve_files keywords master_dir blobs span) of [tr] => Toplevel.modify_init init tr | [] => Toplevel.ignored (#1 (Token.range_of span)) | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected") @@ -191,12 +193,12 @@ local -fun reset_state tr st0 = Toplevel.setmp_thread_position tr (fn () => +fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () => let val name = Toplevel.name_of tr; val res = - if Keyword.is_theory_body name then Toplevel.reset_theory st0 - else if Keyword.is_proof name then Toplevel.reset_proof st0 + if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0 + else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 else NONE; in (case res of @@ -204,8 +206,8 @@ | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st)) end) (); -fun run int tr st = - if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then +fun run keywords int tr st = + if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} (fn () => Toplevel.command_exception int tr st); ([], SOME st)) else Toplevel.command_errors int tr st; @@ -230,7 +232,7 @@ SOME prf => status tr (Proof.status_markup prf) | NONE => ()); -fun eval_state span tr ({malformed, state, ...}: eval_state) = +fun eval_state keywords span tr ({malformed, state, ...}: eval_state) = if malformed then {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} else @@ -238,10 +240,10 @@ val _ = Multithreading.interrupted (); val malformed' = Toplevel.is_malformed tr; - val st = reset_state tr state; + val st = reset_state keywords tr state; val _ = status tr Markup.running; - val (errs1, result) = run true tr st; + val (errs1, result) = run keywords true tr st; val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); val errs = errs1 @ errs2; val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; @@ -262,15 +264,15 @@ in -fun eval init master_dir blobs span eval0 = +fun eval keywords master_dir init blobs span eval0 = let val exec_id = Document_ID.make (); fun process () = let val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) - (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) (); - in eval_state span tr (eval_result eval0) end; + (fn () => read keywords master_dir init blobs span |> Toplevel.exec_id exec_id) (); + in eval_state keywords span tr (eval_result eval0) end; in Eval {exec_id = exec_id, eval_process = memo exec_id process} end; end; @@ -288,7 +290,7 @@ type print_fn = Toplevel.transition -> Toplevel.state -> unit; type print_function = - {command_name: string, args: string list, exec_id: Document_ID.exec} -> + {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; local @@ -310,7 +312,7 @@ in -fun print command_visible command_overlays command_name eval old_prints = +fun print command_visible command_overlays keywords command_name eval old_prints = let val print_functions = Synchronized.value print_functions; @@ -338,7 +340,11 @@ fun new_print name args get_pr = let - val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval}; + val params = + {keywords = keywords, + command_name = command_name, + args = args, + exec_id = eval_exec_id eval}; in (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of Exn.Res NONE => NONE @@ -385,8 +391,8 @@ val _ = print_function "print_state" - (fn {command_name, ...} => - if Keyword.is_printed command_name then + (fn {keywords, command_name, ...} => + if Keyword.is_printed keywords command_name then SOME {delay = NONE, pri = 1, persistent = false, strict = true, print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()} else NONE); diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/PIDE/command_span.ML --- a/src/Pure/PIDE/command_span.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/PIDE/command_span.ML Thu Nov 06 15:47:04 2014 +0100 @@ -10,7 +10,8 @@ datatype span = Span of kind * Token.T list val kind: span -> kind val content: span -> Token.T list - val resolve_files: (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span + val resolve_files: Keyword.keywords -> + (string -> Path.T * Position.T -> Token.file Exn.result list) -> span -> span end; structure Command_Span: COMMAND_SPAN = @@ -49,10 +50,10 @@ in -fun resolve_files read_files span = +fun resolve_files keywords read_files span = (case span of Span (Command_Span (cmd, pos), toks) => - if Keyword.is_theory_load cmd then + if Keyword.is_theory_load keywords cmd then (case find_file (clean_tokens toks) of NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos) | SOME (i, path) => diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/PIDE/document.ML Thu Nov 06 15:47:04 2014 +0100 @@ -466,7 +466,7 @@ is_some (loaded_theory name) orelse can get_header node andalso (not full orelse is_some (get_result node)); -fun last_common state node_required node0 node = +fun last_common keywords state node_required node0 node = let fun update_flags prev (visible, initial) = let @@ -474,7 +474,8 @@ val initial' = initial andalso (case prev of NONE => true - | SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id))); + | SOME command_id => + not (Keyword.is_theory_begin keywords (the_command_name state command_id))); in (visible', initial') end; fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = @@ -495,7 +496,9 @@ val command_overlays = overlays node command_id; val command_name = the_command_name state command_id; in - (case Command.print command_visible command_overlays command_name eval prints of + (case + Command.print command_visible command_overlays keywords command_name eval prints + of SOME prints' => assign_update_new (command_id, SOME (eval, prints')) | NONE => I) end @@ -513,7 +516,7 @@ fun illegal_init _ = error "Illegal theory header after end of theory"; -fun new_exec state node proper_init command_id' (assign_update, command_exec, init) = +fun new_exec keywords state node proper_init command_id' (assign_update, command_exec, init) = if not proper_init andalso is_none init then NONE else let @@ -526,13 +529,14 @@ val span = Lazy.force span0; val eval' = - Command.eval (fn () => the_default illegal_init init span) - (master_directory node) blobs span eval; - val prints' = perhaps (Command.print command_visible command_overlays command_name eval') []; + Command.eval keywords (master_directory node) + (fn () => the_default illegal_init init span) blobs span eval; + val prints' = + perhaps (Command.print command_visible command_overlays keywords command_name eval') []; val exec' = (eval', prints'); val assign_update' = assign_update_new (command_id', SOME exec') assign_update; - val init' = if Keyword.is_theory_begin command_name then NONE else init; + val init' = if Keyword.is_theory_begin keywords command_name then NONE else init; in SOME (assign_update', (command_id', (eval', prints')), init') end; fun removed_execs node0 (command_id, exec_ids) = @@ -558,6 +562,7 @@ deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} (fn () => timeit ("Document.update " ^ name) (fn () => let + val keywords = Keyword.get_keywords (); val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; val node_required = Symtab.defined required name; @@ -574,7 +579,7 @@ val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) - else last_common state node_required node0 node; + else last_common keywords state node_required node0 node; val common_command_exec = the_default_entry node common; val (updated_execs, (command_id', (eval', _)), _) = @@ -583,7 +588,7 @@ iterate_entries_after common (fn ((prev, id), _) => fn res => if not node_required andalso prev = visible_last node then NONE - else new_exec state node proper_init id res) node; + else new_exec keywords state node proper_init id res) node; val assigned_execs = (node0, updated_execs) |-> iterate_entries_after common diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/PIDE/resources.ML Thu Nov 06 15:47:04 2014 +0100 @@ -82,9 +82,10 @@ (case Token.get_files tok of [] => let + val keywords = Keyword.get_keywords (); val master_dir = master_directory thy; val pos = Token.pos_of tok; - val src_paths = Keyword.command_files cmd (Path.explode name); + val src_paths = Keyword.command_files keywords cmd (Path.explode name); in map (Command.read_file master_dir pos) src_paths end | files => map Exn.release files)); @@ -123,17 +124,17 @@ |> put_deps master_dir imports |> fold Thy_Header.declare_keyword keywords; -fun excursion master_dir last_timing init elements = +fun excursion keywords master_dir last_timing init elements = let fun prepare_span span = Command_Span.content span - |> Command.read init master_dir [] + |> Command.read keywords master_dir init [] |> (fn tr => Toplevel.put_timing (last_timing tr) tr); fun element_result span_elem (st, _) = let val elem = Thy_Syntax.map_element prepare_span span_elem; - val (results, st') = Toplevel.element_result elem st; + val (results, st') = Toplevel.element_result keywords elem st; val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); in (results, (st', pos')) end; @@ -151,7 +152,7 @@ val toks = Outer_Syntax.scan keywords text_pos text; val spans = Outer_Syntax.parse_spans toks; - val elements = Thy_Syntax.parse_elements spans; + val elements = Thy_Syntax.parse_elements keywords spans; fun init () = begin_theory master_dir header parents @@ -160,7 +161,7 @@ val (results, thy) = cond_timeit true ("theory " ^ quote name) - (fn () => excursion master_dir last_timing init elements); + (fn () => excursion keywords master_dir last_timing init elements); fun present () = let @@ -171,8 +172,7 @@ warning ("Cannot present theory with skipped proofs: " ^ quote name) else let val tex_source = - Thy_Output.present_thy keywords Keyword.command_tags - (Outer_Syntax.is_markup syntax) res toks + Thy_Output.present_thy keywords (Outer_Syntax.is_markup syntax) res toks |> Buffer.content; in if document then Present.theory_output name tex_source else () end end; diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/Thy/thy_output.ML Thu Nov 06 15:47:04 2014 +0100 @@ -25,7 +25,7 @@ datatype markup = Markup | MarkupEnv | Verbatim val eval_antiq: Keyword.keywords -> Toplevel.state -> Antiquote.antiq -> string val check_text: Symbol_Pos.source -> Toplevel.state -> unit - val present_thy: Keyword.keywords -> (string -> string list) -> (markup -> string -> bool) -> + val present_thy: Keyword.keywords -> (markup -> string -> bool) -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T val pretty_text: Proof.context -> string -> Pretty.T val pretty_term: Proof.context -> term -> Pretty.T @@ -265,8 +265,7 @@ in -fun present_span keywords default_tags span state state' - (tag_stack, active_tag, newline, buffer, present_cont) = +fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) = let val present = fold (fn (tok, (flag, 0)) => Buffer.add (output_token keywords state' tok) @@ -281,7 +280,7 @@ val active_tag' = if is_some tag' then tag' else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE - else try hd (default_tags cmd_name); + else try hd (Keyword.command_tags keywords cmd_name); val edge = (active_tag, active_tag'); val newline' = @@ -351,7 +350,7 @@ in -fun present_thy keywords default_tags is_markup command_results toks = +fun present_thy keywords is_markup command_results toks = let (* tokens *) @@ -423,7 +422,7 @@ (* present commands *) fun present_command tr span st st' = - Toplevel.setmp_thread_position tr (present_span keywords default_tags span st st'); + Toplevel.setmp_thread_position tr (present_span keywords span st st'); fun present _ [] = I | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest; diff -r 1f500b18c4c6 -r cb9b69cca999 src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Thu Nov 06 15:47:04 2014 +0100 @@ -14,7 +14,7 @@ val map_element: ('a -> 'b) -> 'a element -> 'b element val flat_element: 'a element -> 'a list val last_element: 'a element -> 'a - val parse_elements: Command_Span.span list -> Command_Span.span element list + val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list end; structure Thy_Syntax: THY_SYNTAX = @@ -89,23 +89,27 @@ Scan.one (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false); -val proof_atom = - Scan.one - (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => Keyword.is_proof_body name - | _ => true) >> atom; - -fun proof_element x = (command_with Keyword.is_proof_goal -- proof_rest >> element || proof_atom) x -and proof_rest x = (Scan.repeat proof_element -- command_with Keyword.is_qed) x; - -val other_element = - command_with Keyword.is_theory_goal -- proof_rest >> element || - Scan.one not_eof >> atom; +fun parse_element keywords = + let + val proof_atom = + Scan.one + (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => + Keyword.is_proof_body keywords name + | _ => true) >> atom; + fun proof_element x = + (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x + and proof_rest x = + (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x; + in + command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element || + Scan.one not_eof >> atom + end; in -val parse_elements = +fun parse_elements keywords = Source.of_list #> - Source.source stopper (Scan.bulk other_element) #> + Source.source stopper (Scan.bulk (parse_element keywords)) #> Source.exhaust; end; diff -r 1f500b18c4c6 -r cb9b69cca999 src/Tools/try.ML --- a/src/Tools/try.ML Thu Nov 06 15:42:34 2014 +0100 +++ b/src/Tools/try.ML Thu Nov 06 15:47:04 2014 +0100 @@ -96,8 +96,8 @@ fun print_function ((name, (weight, auto, tool)): tool) = Command.print_function ("auto_" ^ name) - (fn {command_name, ...} => - if Keyword.is_theory_goal command_name andalso Options.default_bool auto then + (fn {keywords, command_name, ...} => + if Keyword.is_theory_goal keywords command_name andalso Options.default_bool auto then SOME {delay = SOME (seconds (Options.default_real @{system_option auto_time_start})), pri = ~ weight,