diff --git a/src/HOL/SMT_Examples/boogie.ML b/src/HOL/SMT_Examples/boogie.ML --- a/src/HOL/SMT_Examples/boogie.ML +++ b/src/HOL/SMT_Examples/boogie.ML @@ -1,278 +1,278 @@ (* Title: HOL/SMT_Examples/boogie.ML Author: Sascha Boehme, TU Muenchen Proving Boogie-generated verification conditions. *) signature BOOGIE = sig val boogie_prove: theory -> string list -> unit end; structure Boogie: BOOGIE = struct (* utility functions *) val as_int = fst o read_int o raw_explode val isabelle_name = let fun purge s = if Symbol.is_letter s orelse Symbol.is_digit s then s else (case s of "." => "_o_" | "_" => "_n_" | "$" => "_S_" | "@" => "_G_" | "#" => "_H_" | "^" => "_T_" | _ => ("_" ^ string_of_int (ord s) ^ "_")) in prefix "b_" o translate_string purge end (* context *) type context = typ Symtab.table * (term * bool) Symtab.table * term list * term list val empty_context: context = (Symtab.empty, Symtab.empty, [], []) fun add_type name (tds, fds, axs, vcs) = let val T = TFree (isabelle_name name, \<^sort>\type\) val tds' = Symtab.update (name, T) tds in (tds', fds, axs, vcs) end fun add_func name Ts T unique (tds, fds, axs, vcs) = let val t = Free (isabelle_name name, Ts ---> T) val fds' = Symtab.update (name, (t, unique)) fds in (tds, fds', axs, vcs) end fun add_axiom t (tds, fds, axs, vcs) = (tds, fds, t :: axs, vcs) fun add_vc t (tds, fds, axs, vcs) = (tds, fds, axs, t :: vcs) fun lookup_type (tds, _, _, _) name = (case Symtab.lookup tds name of SOME T => T | NONE => error "Undeclared type") fun lookup_func (_, fds, _, _) name = (case Symtab.lookup fds name of SOME t_unique => t_unique | NONE => error "Undeclared function") (* constructors *) fun mk_var name T = Free ("V_" ^ isabelle_name name, T) fun mk_arrayT (Ts, T) = Type (\<^type_name>\fun\, [HOLogic.mk_tupleT Ts, T]) fun mk_binary t (t1, t2) = t $ t1 $ t2 fun mk_nary _ t [] = t | mk_nary f _ ts = uncurry (fold_rev f) (split_last ts) fun mk_distinct [] = \<^const>\HOL.True\ | mk_distinct [_] = \<^const>\HOL.True\ | mk_distinct (t :: ts) = let fun mk_noteq u u' = HOLogic.mk_conj (HOLogic.mk_not (HOLogic.mk_eq (t, u)), u') in fold_rev mk_noteq ts (mk_distinct ts) end fun mk_store m k v = let val mT = Term.fastype_of m and kT = Term.fastype_of k val vT = Term.fastype_of v in Const (\<^const_name>\fun_upd\, mT --> kT --> vT --> mT) $ m $ k $ v end fun mk_quant q (Free (x, T)) t = q T $ absfree (x, T) t | mk_quant _ t _ = raise TERM ("bad variable", [t]) val patternT = \<^typ>\SMT.pattern\ fun mk_pat t = Const (\<^const_name>\SMT.pat\, Term.fastype_of t --> patternT) $ t fun mk_pattern [] = raise TERM ("mk_pattern", []) | mk_pattern ts = SMT_Util.mk_symb_list patternT (map mk_pat ts) fun mk_trigger [] t = t | mk_trigger pss t = \<^term>\SMT.trigger\ $ SMT_Util.mk_symb_list \<^typ>\SMT.pattern SMT.symb_list\ (map mk_pattern pss) $ t (* parser *) fun repeat f n ls = let fun apply (xs, ls) = f ls |>> (fn x => x :: xs) in funpow (as_int n) apply ([], ls) |>> rev end fun parse_type _ (["bool"] :: ls) = (\<^typ>\bool\, ls) | parse_type _ (["int"] :: ls) = (\<^typ>\int\, ls) | parse_type cx (["array", arity] :: ls) = repeat (parse_type cx) arity ls |>> mk_arrayT o split_last | parse_type cx (("type-con" :: name :: _) :: ls) = (lookup_type cx name, ls) | parse_type _ _ = error "Bad type" fun parse_expr _ (["true"] :: ls) = (\<^term>\True\, ls) | parse_expr _ (["false"] :: ls) = (\<^term>\False\, ls) | parse_expr cx (["not"] :: ls) = parse_expr cx ls |>> HOLogic.mk_not | parse_expr cx (["and", n] :: ls) = parse_nary_expr cx n HOLogic.mk_conj \<^term>\True\ ls | parse_expr cx (["or", n] :: ls) = parse_nary_expr cx n HOLogic.mk_disj \<^term>\False\ ls | parse_expr cx (["implies"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\HOL.implies\) ls | parse_expr cx (["="] :: ls) = parse_bin_expr cx HOLogic.mk_eq ls | parse_expr cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name | parse_expr cx (["fun", name, n] :: ls) = let val (t, _) = lookup_func cx name in repeat (parse_expr cx) n ls |>> curry Term.list_comb t end | parse_expr cx (("label" :: _) :: ls) = parse_expr cx ls | parse_expr _ (["int-num", n] :: ls) = (HOLogic.mk_number \<^typ>\int\ (as_int n), ls) | parse_expr cx (["<"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(<) :: int => _\) ls | parse_expr cx (["<="] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(<=) :: int => _\) ls | parse_expr cx ([">"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(<) :: int => _\o swap) ls | parse_expr cx ([">="] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(<=) :: int => _\ o swap) ls | parse_expr cx (["+"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(+) :: int => _\) ls | parse_expr cx (["-"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(-) :: int => _\) ls | parse_expr cx (["*"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\(*) :: int => _\) ls | parse_expr cx (["/"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\boogie_div\) ls | parse_expr cx (["%"] :: ls) = parse_bin_expr cx (mk_binary \<^term>\boogie_mod\) ls | parse_expr cx (["select", n] :: ls) = repeat (parse_expr cx) n ls |>> (fn ts => hd ts $ HOLogic.mk_tuple (tl ts)) | parse_expr cx (["store", n] :: ls) = repeat (parse_expr cx) n ls |>> split_last |>> (fn (ts, t) => mk_store (hd ts) (HOLogic.mk_tuple (tl ts)) t) | parse_expr cx (["forall", vars, pats, atts] :: ls) = parse_quant cx HOLogic.all_const vars pats atts ls | parse_expr cx (["exists", vars, pats, atts] :: ls) = parse_quant cx HOLogic.exists_const vars pats atts ls | parse_expr _ _ = error "Bad expression" and parse_bin_expr cx f ls = ls |> parse_expr cx ||>> parse_expr cx |>> f and parse_nary_expr cx n f c ls = repeat (parse_expr cx) n ls |>> mk_nary (curry f) c and parse_quant cx q vars pats atts ls = let val ((((vs, pss), _), t), ls') = ls |> repeat (parse_var cx) vars ||>> repeat (parse_pat cx) pats ||>> repeat (parse_attr cx) atts ||>> parse_expr cx in (fold_rev (mk_quant q) vs (mk_trigger pss t), ls') end and parse_var cx (["var", name] :: ls) = parse_type cx ls |>> mk_var name | parse_var _ _ = error "Bad variable" and parse_pat cx (["pat", n] :: ls) = repeat (parse_expr cx) n ls | parse_pat _ _ = error "Bad pattern" and parse_attr cx (["attribute", name, n] :: ls) = let fun attr (["expr-attr"] :: ls) = parse_expr cx ls |>> K () | attr (("string-attr" :: _) :: ls) = ((), ls) | attr _ = error "Bad attribute value" in repeat attr n ls |>> K name end | parse_attr _ _ = error "Bad attribute" fun parse_func cx arity n ls = let val ((Ts, atts), ls') = ls |> repeat (parse_type cx) arity ||>> repeat (parse_attr cx) n val unique = member (op =) atts "unique" in ((split_last Ts, unique), ls') end fun parse_decl (("type-decl" :: name :: _) :: ls) cx = (ls, add_type name cx) | parse_decl (["fun-decl", name, arity, n] :: ls) cx = let val (((Ts, T), unique), ls') = parse_func cx arity n ls in (ls', add_func name Ts T unique cx) end | parse_decl (("axiom" :: _) :: ls) cx = let val (t, ls') = parse_expr cx ls in (ls', add_axiom t cx) end | parse_decl (("var-decl" :: _) :: ls) cx = parse_type cx ls |> snd |> rpair cx | parse_decl (("vc" :: _) :: ls) cx = let val (t, ls') = parse_expr cx ls in (ls', add_vc t cx) end | parse_decl _ _ = error "Bad declaration" fun parse_lines [] cx = cx | parse_lines ls cx = parse_decl ls cx |-> parse_lines (* splitting of text lines into a lists of tokens *) fun is_blank c = (c = " " orelse c = "\t" orelse c = "\r" orelse c = "\n") val token_lines = map (String.tokens (is_blank o str)) #> filter (fn [] => false | _ => true) (* proving verification conditions *) fun add_unique_axioms (tds, fds, axs, vcs) = Symtab.fold (fn (_, (t, true)) => cons t | _ => I) fds [] |> map (swap o Term.dest_Free) |> AList.group (op =) |> map (fn (T, ns) => mk_distinct (map (Free o rpair T) ns)) |> (fn axs' => (tds, fds, axs' @ axs, vcs)) fun build_proof_context thy (tds, fds, axs, vcs) = let val vc = (case vcs of [vc] => vc | _ => error "Bad number of verification conditions") in Proof_Context.init_global thy |> Symtab.fold (fn (_, T) => Variable.declare_typ T) tds |> Symtab.fold (fn (_, (t, _)) => Variable.declare_term t) fds |> fold Variable.declare_term axs |> fold Variable.declare_term vcs |> pair (map HOLogic.mk_Trueprop axs, HOLogic.mk_Trueprop vc) end val boogie_rules = [@{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}] @ [@{thm fun_upd_same}, @{thm fun_upd_apply}] fun boogie_tac ctxt axioms = ALLGOALS (SMT_Solver.smt_tac ctxt (boogie_rules @ axioms)) fun boogie_prove thy lines = let val ((axioms, vc), ctxt) = empty_context |> parse_lines (token_lines lines) |> add_unique_axioms |> build_proof_context thy val _ = Goal.prove ctxt [] axioms vc (fn {prems, context} => boogie_tac context prems) val _ = writeln "Verification condition proved successfully" in () end (* Isar command *) val _ = Outer_Syntax.command \<^command_keyword>\boogie_file\ "prove verification condition from .b2i file" - (Resources.provide_parse_files "boogie_file" >> (fn files => + (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (fn thy => let - val ([{lines, ...}], thy') = files thy; + val ({lines, ...}, thy') = get_file thy; val _ = boogie_prove thy' lines; in thy' end))) end; diff --git a/src/HOL/SPARK/Tools/spark_commands.ML b/src/HOL/SPARK/Tools/spark_commands.ML --- a/src/HOL/SPARK/Tools/spark_commands.ML +++ b/src/HOL/SPARK/Tools/spark_commands.ML @@ -1,152 +1,152 @@ (* Title: HOL/SPARK/Tools/spark_commands.ML Author: Stefan Berghofer Copyright: secunet Security Networks AG Isar commands for handling SPARK/Ada verification conditions. *) structure SPARK_Commands: sig end = struct fun spark_open header (files, prfx) thy = let val ([{src_path, lines = vc_lines, pos = vc_pos, ...}: Token.file, {lines = fdl_lines, pos = fdl_pos, ...}, {lines = rls_lines, pos = rls_pos, ...}], thy') = files thy; val path = fst (Path.split_ext src_path); in SPARK_VCs.set_vcs (snd (Fdl_Parser.parse_declarations fdl_pos (cat_lines fdl_lines))) (Fdl_Parser.parse_rules rls_pos (cat_lines rls_lines)) (snd (Fdl_Parser.parse_vcs header vc_pos (cat_lines vc_lines))) path prfx thy' end; fun add_proof_fun_cmd pf thy = let val ctxt = Proof_Context.init_global thy in SPARK_VCs.add_proof_fun (fn optT => Syntax.parse_term ctxt #> the_default I (Option.map Type.constraint optT) #> Syntax.check_term ctxt) pf thy end; fun add_spark_type_cmd (s, (raw_typ, cmap)) thy = SPARK_VCs.add_type (s, (Syntax.read_typ_global thy raw_typ, cmap)) thy; fun get_vc thy vc_name = (case SPARK_VCs.lookup_vc thy false vc_name of SOME (ctxt, (_, proved, ctxt', stmt)) => if is_some proved then error ("The verification condition " ^ quote vc_name ^ " has already been proved.") else (ctxt @ [ctxt'], stmt) | NONE => error ("There is no verification condition " ^ quote vc_name ^ ".")); fun prove_vc vc_name lthy = let val thy = Proof_Context.theory_of lthy; val (ctxt, stmt) = get_vc thy vc_name in Specification.theorem true Thm.theoremK NONE (fn thmss => (Local_Theory.background_theory (SPARK_VCs.mark_proved vc_name (flat thmss)))) (Binding.name vc_name, []) [] ctxt stmt false lthy end; fun string_of_status NONE = "(unproved)" | string_of_status (SOME _) = "(proved)"; fun show_status thy (p, f) = let val (context, defs, vcs) = SPARK_VCs.get_vcs thy true; val vcs' = AList.coalesce (op =) (map_filter (fn (name, (trace, status, ctxt, stmt)) => if p status then SOME (trace, (name, status, ctxt, stmt)) else NONE) vcs); val ctxt = thy |> Proof_Context.init_global |> Context.proof_map (fold Element.init context) in [Pretty.str "Context:", Pretty.chunks (maps (Element.pretty_ctxt ctxt) context), Pretty.str "Definitions:", Pretty.chunks (map (fn (b, th) => Pretty.block [Binding.pretty b, Pretty.str ":", Pretty.brk 1, Thm.pretty_thm ctxt th]) defs), Pretty.str "Verification conditions:", Pretty.chunks2 (maps (fn (trace, vcs'') => Pretty.str trace :: map (fn (name, status, context', stmt) => Pretty.big_list (name ^ " " ^ f status) (Element.pretty_ctxt ctxt context' @ Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |> Pretty.writeln_chunks2 end; val _ = Outer_Syntax.command \<^command_keyword>\spark_open_vcg\ "open a new SPARK environment and load a SPARK-generated .vcg file" - (Resources.provide_parse_files "spark_open_vcg" -- Parse.parname + (Resources.provide_parse_files (Resources.extensions ["vcg", "fdl", "rls"]) -- Parse.parname >> (Toplevel.theory o spark_open Fdl_Lexer.vcg_header)); val _ = Outer_Syntax.command \<^command_keyword>\spark_open\ "open a new SPARK environment and load a SPARK-generated .siv file" - (Resources.provide_parse_files "spark_open" -- Parse.parname + (Resources.provide_parse_files (Resources.extensions ["siv", "fdl", "rls"]) -- Parse.parname >> (Toplevel.theory o spark_open Fdl_Lexer.siv_header)); val pfun_type = Scan.option (Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name); val _ = Outer_Syntax.command \<^command_keyword>\spark_proof_functions\ "associate SPARK proof functions with terms" (Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >> (Toplevel.theory o fold add_proof_fun_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\spark_types\ "associate SPARK types with types" (Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ -- Scan.optional (Args.parens (Parse.list1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.name)))) [])) >> (Toplevel.theory o fold add_spark_type_cmd)); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\spark_vc\ "enter into proof mode for a specific verification condition" (Parse.name >> prove_vc); val _ = Outer_Syntax.command \<^command_keyword>\spark_status\ "show the name and state of all loaded verification conditions" (Scan.optional (Args.parens ( Args.$$$ "proved" >> K (is_some, K "") || Args.$$$ "unproved" >> K (is_none, K ""))) (K true, string_of_status) >> (fn args => Toplevel.keep (fn state => show_status (Toplevel.theory_of state) args))) val _ = Outer_Syntax.command \<^command_keyword>\spark_end\ "close the current SPARK environment" (Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.reserved "incomplete" --| \<^keyword>\)\) >> K true) false >> (Toplevel.theory o SPARK_VCs.close)); val _ = Theory.setup (Theory.at_end (fn thy => let val _ = SPARK_VCs.is_closed thy orelse error ("Found the end of the theory, " ^ "but the last SPARK environment is still open.") in NONE end)); end; diff --git a/src/Pure/Isar/keyword.ML b/src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML +++ b/src/Pure/Isar/keyword.ML @@ -1,297 +1,285 @@ (* Title: Pure/Isar/keyword.ML Author: Makarius Isar keyword classification. *) signature KEYWORD = sig val diag: string val document_heading: string val document_body: string val document_raw: string val thy_begin: string val thy_end: string val thy_decl: string val thy_decl_block: string val thy_defn: string val thy_stmt: string val thy_load: string val thy_goal: string val thy_goal_defn: string val thy_goal_stmt: string val qed: string val qed_script: string val qed_block: string val qed_global: string val prf_goal: string val prf_block: string val next_block: string val prf_open: string val prf_close: string val prf_chain: string val prf_decl: string val prf_asm: string val prf_asm_goal: string val prf_script: string val prf_script_goal: string val prf_script_asm_goal: string val before_command: string val quasi_command: string - type spec = (string * string list) * string list + type spec = string * string list val no_spec: spec val before_command_spec: spec val quasi_command_spec: spec val document_heading_spec: spec val document_body_spec: spec type keywords val minor_keywords: keywords -> Scan.lexicon val major_keywords: keywords -> Scan.lexicon val no_command_keywords: keywords -> keywords val empty_keywords: keywords val merge_keywords: keywords * keywords -> keywords val add_keywords: ((string * Position.T) * spec) list -> keywords -> keywords val is_keyword: keywords -> string -> bool val is_command: keywords -> string -> bool val is_literal: keywords -> string -> bool val dest_commands: keywords -> string list val command_markup: keywords -> string -> Markup.T option val command_kind: keywords -> string -> string option - val command_files: keywords -> string -> Path.T -> Path.T list val command_tags: keywords -> string -> string list val is_vacuous: keywords -> string -> bool val is_diag: keywords -> string -> bool val is_document_heading: keywords -> string -> bool val is_document_body: keywords -> string -> bool val is_document_raw: keywords -> string -> bool val is_document: keywords -> string -> bool val is_theory_end: 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_proof_open: keywords -> string -> bool val is_proof_close: keywords -> string -> bool val is_proof_asm: keywords -> string -> bool val is_improper: keywords -> string -> bool val is_printed: keywords -> string -> bool end; structure Keyword: KEYWORD = struct (** keyword classification **) (* kinds *) val diag = "diag"; val document_heading = "document_heading"; val document_body = "document_body"; val document_raw = "document_raw"; val thy_begin = "thy_begin"; val thy_end = "thy_end"; val thy_decl = "thy_decl"; val thy_decl_block = "thy_decl_block"; val thy_defn = "thy_defn"; val thy_stmt = "thy_stmt"; val thy_load = "thy_load"; val thy_goal = "thy_goal"; val thy_goal_defn = "thy_goal_defn"; val thy_goal_stmt = "thy_goal_stmt"; val qed = "qed"; val qed_script = "qed_script"; val qed_block = "qed_block"; val qed_global = "qed_global"; val prf_goal = "prf_goal"; val prf_block = "prf_block"; val next_block = "next_block"; val prf_open = "prf_open"; val prf_close = "prf_close"; val prf_chain = "prf_chain"; val prf_decl = "prf_decl"; val prf_asm = "prf_asm"; val prf_asm_goal = "prf_asm_goal"; val prf_script = "prf_script"; val prf_script_goal = "prf_script_goal"; val prf_script_asm_goal = "prf_script_asm_goal"; val before_command = "before_command"; val quasi_command = "quasi_command"; val command_kinds = [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; (* specifications *) -type spec = (string * string list) * string list; +type spec = string * string list; -val no_spec: spec = (("", []), []); -val before_command_spec: spec = ((before_command, []), []); -val quasi_command_spec: spec = ((quasi_command, []), []); -val document_heading_spec: spec = (("document_heading", []), ["document"]); -val document_body_spec: spec = (("document_body", []), ["document"]); +val no_spec: spec = ("", []); +val before_command_spec: spec = (before_command, []); +val quasi_command_spec: spec = (quasi_command, []); +val document_heading_spec: spec = ("document_heading", ["document"]); +val document_body_spec: spec = ("document_body", ["document"]); type entry = {pos: Position.T, id: serial, kind: string, - files: string list, (*extensions of embedded files*) tags: string list}; -fun check_spec pos ((kind, files), tags) : entry = +fun check_spec pos (kind, tags) : entry = if not (member (op =) command_kinds kind) then error ("Unknown outer syntax keyword kind " ^ quote kind) - else if not (null files) andalso kind <> thy_load then - error ("Illegal specification of files for " ^ quote kind) - else {pos = pos, id = serial (), kind = kind, files = files, tags = tags}; + else {pos = pos, id = serial (), kind = kind, tags = tags}; (** keyword tables **) (* type keywords *) datatype keywords = Keywords of {minor: Scan.lexicon, major: Scan.lexicon, commands: entry Symtab.table}; fun minor_keywords (Keywords {minor, ...}) = minor; fun major_keywords (Keywords {major, ...}) = major; fun make_keywords (minor, major, commands) = Keywords {minor = minor, major = major, commands = commands}; fun map_keywords f (Keywords {minor, major, commands}) = make_keywords (f (minor, major, commands)); val no_command_keywords = map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); (* build keywords *) val empty_keywords = make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty); fun merge_keywords (Keywords {minor = minor1, major = major1, commands = commands1}, Keywords {minor = minor2, major = major2, commands = commands2}) = make_keywords (Scan.merge_lexicons (minor1, minor2), Scan.merge_lexicons (major1, major2), Symtab.merge (K true) (commands1, commands2)); val add_keywords = - fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) => + fold (fn ((name, pos), spec as (kind, _)) => map_keywords (fn (minor, major, commands) => if kind = "" orelse kind = before_command orelse kind = quasi_command then let val minor' = Scan.extend_lexicon (Symbol.explode name) minor; in (minor', major, commands) end else let val entry = check_spec pos spec; val major' = Scan.extend_lexicon (Symbol.explode name) major; val commands' = Symtab.update (name, entry) commands; in (minor, major', commands') end)); (* keyword status *) fun is_keyword keywords s = Scan.is_literal (minor_keywords keywords) (Symbol.explode s); fun is_command (Keywords {commands, ...}) = Symtab.defined commands; fun is_literal keywords = is_keyword keywords orf is_command keywords; fun dest_commands (Keywords {commands, ...}) = Symtab.keys commands; (* command keywords *) fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands; fun command_markup keywords name = lookup_command keywords name |> Option.map (fn {pos, id, ...} => Markup.properties (Position.entity_properties_of false id pos) (Markup.entity Markup.command_keywordN name)); fun command_kind keywords = Option.map #kind o lookup_command keywords; -fun command_files keywords name path = - (case lookup_command keywords name of - NONE => [] - | SOME {kind, files, ...} => - if kind <> thy_load then [] - else if null files then [path] - else map (fn ext => Path.ext ext path) files); - fun command_tags keywords name = (case lookup_command keywords name of SOME {tags, ...} => tags | NONE => []); (* command categories *) fun command_category ks = let val tab = Symtab.make_set ks; fun pred keywords name = (case lookup_command keywords name of NONE => false | SOME {kind, ...} => Symtab.defined tab kind); in pred end; val is_vacuous = command_category [diag, document_heading, document_body, document_raw]; val is_diag = command_category [diag]; val is_document_heading = command_category [document_heading]; val is_document_body = command_category [document_body]; val is_document_raw = command_category [document_raw]; val is_document = command_category [document_heading, document_body, document_raw]; val is_theory_end = command_category [thy_end]; val is_theory_load = command_category [thy_load]; val is_theory = command_category [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_theory_body = command_category [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof = command_category [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_proof_body = command_category [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal]; val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt]; val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal]; val is_qed = command_category [qed, qed_script, qed_block]; val is_qed_global = command_category [qed_global]; val is_proof_open = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal, prf_open]; val is_proof_close = command_category [qed, qed_script, qed_block, prf_close]; val is_proof_asm = command_category [prf_asm, prf_asm_goal]; val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal]; fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; end; diff --git a/src/Pure/ML/ml_file.ML b/src/Pure/ML/ml_file.ML --- a/src/Pure/ML/ml_file.ML +++ b/src/Pure/ML/ml_file.ML @@ -1,39 +1,39 @@ (* Title: Pure/ML/ml_file.ML Author: Makarius Commands to load ML files. *) signature ML_FILE = sig - val command: string -> bool option -> (theory -> Token.file list) -> + val command: string -> bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition - val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition - val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition + val ML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition + val SML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition end; structure ML_File: ML_FILE = struct -fun command environment debug files = Toplevel.generic_theory (fn gthy => +fun command environment debug get_file = Toplevel.generic_theory (fn gthy => let - val [file: Token.file] = files (Context.theory_of gthy); + val file = get_file (Context.theory_of gthy); val provide = Resources.provide_file file; val source = Token.file_source file; val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source); val flags: ML_Compiler.flags = {environment = environment, redirect = true, verbose = true, debug = debug, writeln = writeln, warning = warning}; in gthy |> ML_Context.exec (fn () => ML_Context.eval_source flags source) |> Local_Theory.propagate_ml_env |> Context.mapping provide (Local_Theory.background_theory provide) end); val ML = command ""; val SML = command ML_Env.SML; end; diff --git a/src/Pure/PIDE/command.ML b/src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML +++ b/src/Pure/PIDE/command.ML @@ -1,507 +1,498 @@ (* Title: Pure/PIDE/command.ML Author: Makarius Prover command execution: read -- eval -- print. *) signature COMMAND = sig - type blob = (string * (SHA1.digest * string list) option) Exn.result + type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option} val read_file: Path.T -> Position.T -> Path.T -> Token.file val read_thy: Toplevel.state -> theory val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> - blob list * int -> Token.T list -> Toplevel.transition + blob Exn.result list * int -> Token.T list -> Toplevel.transition type eval val eval_command_id: eval -> Document_ID.command val eval_exec_id: eval -> Document_ID.exec val eval_eq: eval * eval -> bool val eval_running: eval -> bool val eval_finished: eval -> bool val eval_result_command: eval -> Toplevel.transition val eval_result_state: eval -> Toplevel.state val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> - blob list * int -> Document_ID.command -> Token.T list -> eval -> eval + blob Exn.result list * int -> Document_ID.command -> Token.T list -> eval -> eval type print type print_fn = Toplevel.transition -> Toplevel.state -> unit val print0: {pri: int, print_fn: print_fn} -> eval -> print val print: bool -> (string * string list) list -> Keyword.keywords -> string -> eval -> print list -> print list option val parallel_print: print -> bool type print_function = {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 type exec = eval * print list val init_exec: theory option -> exec val no_exec: exec val exec_ids: exec option -> Document_ID.exec list val exec: Document_ID.execution -> exec -> unit val exec_parallel_prints: Document_ID.execution -> Future.task list -> exec -> exec option end; structure Command: COMMAND = struct (** main phases of execution **) fun task_context group f = f |> Future.interruptible_task |> Future.task_context "Command.run_process" group; (* read *) -type blob = - (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) +type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}; fun read_file_node file_node master_dir pos src_path = let val _ = if Context_Position.pide_reports () then Position.report pos Markup.language_path else (); val _ = (case try Url.explode file_node of NONE => () | SOME (Url.File _) => () | _ => error ("Prover cannot load remote file " ^ Markup.markup (Markup.path file_node) (quote file_node))); val full_path = File.check_file (File.full_path master_dir src_path); val text = File.read full_path; val lines = split_lines text; val digest = SHA1.digest text; val file_pos = Position.copy_id pos (Path.position full_path); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end handle ERROR msg => error (msg ^ Position.here pos); val read_file = read_file_node ""; local fun blob_file src_path lines digest file_node = let val file_pos = Position.file file_node |> (case Position.get_id (Position.thread_data ()) of NONE => I | SOME exec_id => Position.put_id exec_id); in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end -fun resolve_files keywords master_dir (blobs, blobs_index) toks = +fun resolve_files master_dir (blobs, blobs_index) toks = (case Outer_Syntax.parse_spans toks of [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] => (case try (nth toks) blobs_index of SOME tok => let val pos = Token.pos_of tok; - val path = Path.explode (Token.content_of tok) - handle ERROR msg => error (msg ^ Position.here pos); - fun make_file src_path (Exn.Res (file_node, NONE)) = + fun make_file (Exn.Res {file_node, src_path, content = NONE}) = Exn.interruptible_capture (fn () => read_file_node file_node master_dir pos src_path) () - | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = + | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) = (Position.report pos Markup.language_path; Exn.Res (blob_file src_path lines digest file_node)) - | make_file _ (Exn.Exn e) = Exn.Exn e; - val src_paths = Keyword.command_files keywords cmd path; - val files = - if null blobs then - map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) - else if length src_paths = length blobs then - map2 make_file src_paths blobs - else error ("Misalignment of inlined files" ^ Position.here pos); + | make_file (Exn.Exn e) = Exn.Exn e; + val files = map make_file blobs; in toks |> map_index (fn (i, tok) => if i = blobs_index then Token.put_files files tok else tok) end | NONE => toks) | _ => toks); fun reports_of_token keywords tok = let val malformed_symbols = Input.source_explode (Token.input_of tok) |> map_filter (fn (sym, pos) => if Symbol.is_malformed sym then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE); val is_malformed = Token.is_error tok orelse not (null malformed_symbols); val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; in (is_malformed, reports) end; in fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy; fun read keywords thy master_dir init blobs_info span = let val command_reports = Outer_Syntax.command_reports thy; val core_range = Token.range_of (drop_suffix Token.is_ignored span); val pos = (case find_first Token.is_command span of SOME tok => Token.pos_of tok | NONE => #1 core_range); val token_reports = map (reports_of_token keywords) span; val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span); val verbatim = span |> map_filter (fn tok => if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE); val _ = if null verbatim then () else legacy_feature ("Old-style {* verbatim *} token -- use \cartouche\ instead" ^ Position.here_list verbatim); in if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax" - else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span) + else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span) end; end; (* eval *) type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state}; fun init_eval_state opt_thy = {failed = false, command = Toplevel.empty, state = (case opt_thy of NONE => Toplevel.init_toplevel () | SOME thy => Toplevel.theory_toplevel thy)}; datatype eval = Eval of {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy}; fun eval_command_id (Eval {command_id, ...}) = command_id; fun eval_exec_id (Eval {exec_id, ...}) = exec_id; val eval_eq = op = o apply2 eval_exec_id; val eval_running = Execution.is_running_exec o eval_exec_id; fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process; fun eval_result (Eval {eval_process, ...}) = Exn.release (Lazy.finished_result eval_process); val eval_result_command = #command o eval_result; val eval_result_state = #state o eval_result; local 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 keywords name then Toplevel.reset_theory st0 else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 else if Keyword.is_theory_end keywords name then (case Toplevel.reset_notepad st0 of NONE => Toplevel.reset_theory st0 | some => some) else NONE; in (case res of NONE => st0 | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st)) end) (); fun run keywords int tr st = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then let val (tr1, tr2) = Toplevel.fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} (fn () => Toplevel.command_exception int tr1 st); in Toplevel.command_errors int tr2 st end else Toplevel.command_errors int tr st; fun check_token_comments ctxt tok = (Thy_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); []) handle exn => if Exn.is_interrupt exn then Exn.reraise exn else Runtime.exn_messages exn; fun check_span_comments ctxt span tr = Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) (); fun report tr m = Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); fun status tr m = Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) (); fun command_indent tr st = (case try Toplevel.proof_of st of SOME prf => let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then (case try Proof.goal prf of SOME {goal, ...} => let val n = Thm.nprems_of goal in if n > 1 then report tr (Markup.command_indent (n - 1)) else () end | NONE => ()) else () end | NONE => ()); fun eval_state keywords span tr ({state, ...}: eval_state) = let val _ = Thread_Attributes.expose_interrupt (); val st = reset_state keywords tr state; val _ = command_indent tr st; val _ = status tr Markup.running; val (errs1, result) = run keywords true tr st; val errs2 = (case result of NONE => [] | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr); val errs = errs1 @ errs2; val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; in (case result of NONE => let val _ = status tr Markup.failed; val _ = status tr Markup.finished; val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else (); in {failed = true, command = tr, state = st} end | SOME st' => let val _ = if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso can (Toplevel.end_theory Position.none) st' then status tr Markup.finalized else (); val _ = status tr Markup.finished; in {failed = false, command = tr, state = st'} end) end; in fun eval keywords master_dir init blobs_info command_id span eval0 = let val exec_id = Document_ID.make (); fun process () = let val eval_state0 = eval_result eval0; val thy = read_thy (#state eval_state0); val tr = Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) (fn () => read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) (); in eval_state keywords span tr eval_state0 end; in Eval {command_id = command_id, exec_id = exec_id, eval_process = Lazy.lazy_name "Command.eval" process} end; end; (* print *) datatype print = Print of {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, exec_id: Document_ID.exec, print_process: unit lazy}; fun print_exec_id (Print {exec_id, ...}) = exec_id; val print_eq = op = o apply2 print_exec_id; type print_fn = Toplevel.transition -> Toplevel.state -> unit; type print_function = {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 val print_functions = Synchronized.var "Command.print_functions" ([]: (string * print_function) list); fun print_error tr opt_context e = (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn); fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process; fun print_persistent (Print {persistent, ...}) = persistent; val overlay_ord = prod_ord string_ord (list_ord string_ord); fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval = let val exec_id = Document_ID.make (); fun process () = let val {failed, command, state = st', ...} = eval_result eval; val tr = Toplevel.exec_id exec_id command; val opt_context = try Toplevel.generic_theory_of st'; in if failed andalso strict then () else print_error tr opt_context (fn () => print_fn tr st') end; in Print { name = name, args = args, delay = delay, pri = pri, persistent = persistent, exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process} end; fun bad_print name_args exn = make_print name_args {delay = NONE, pri = 0, persistent = false, strict = false, print_fn = fn _ => fn _ => Exn.reraise exn}; in fun print0 {pri, print_fn} = make_print ("", [serial_string ()]) {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn}; fun print command_visible command_overlays keywords command_name eval old_prints = let val print_functions = Synchronized.value print_functions; fun new_print (name, args) get_pr = let 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 | Exn.Res (SOME pr) => SOME (make_print (name, args) pr eval) | Exn.Exn exn => SOME (bad_print (name, args) exn eval)) end; fun get_print (name, args) = (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of NONE => (case AList.lookup (op =) print_functions name of NONE => SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval) | SOME get_pr => new_print (name, args) get_pr) | some => some); val retained_prints = filter (fn print => print_finished print andalso print_persistent print) old_prints; val visible_prints = if command_visible then fold (fn (name, _) => cons (name, [])) print_functions command_overlays |> sort_distinct overlay_ord |> map_filter get_print else []; val new_prints = visible_prints @ retained_prints; in if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints end; fun parallel_print (Print {pri, ...}) = pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print"); fun print_function name f = Synchronized.change print_functions (fn funs => (if name = "" then error "Unnamed print function" else (); if not (AList.defined (op =) funs name) then () else warning ("Redefining command print function: " ^ quote name); AList.update (op =) (name, f) funs)); fun no_print_function name = Synchronized.change print_functions (filter_out (equal name o #1)); end; val _ = print_function "Execution.print" (fn {args, exec_id, ...} => if null args then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, print_fn = fn _ => fn _ => Execution.fork_prints exec_id} else NONE); val _ = print_function "print_state" (fn {keywords, command_name, ...} => if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name then SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false, print_fn = fn _ => fn st => if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) else ()} else NONE); (* combined execution *) type exec = eval * print list; fun init_exec opt_thy : exec = (Eval {command_id = Document_ID.none, exec_id = Document_ID.none, eval_process = Lazy.value (init_eval_state opt_thy)}, []); val no_exec = init_exec NONE; fun exec_ids NONE = [] | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; local fun run_process execution_id exec_id process = let val group = Future.worker_subgroup () in if Execution.running execution_id exec_id [group] then ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ()) else () end; fun ignore_process process = Lazy.is_running process orelse Lazy.is_finished process; fun run_eval execution_id (Eval {exec_id, eval_process, ...}) = if Lazy.is_finished eval_process then () else run_process execution_id exec_id eval_process; fun fork_print execution_id deps (Print {name, delay, pri, exec_id, print_process, ...}) = let val group = Future.worker_subgroup (); fun fork () = ignore ((singleton o Future.forks) {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} (fn () => if ignore_process print_process then () else run_process execution_id exec_id print_process)); in (case delay of NONE => fork () | SOME d => ignore (Event_Timer.request {physical = true} (Time.now () + d) fork)) end; fun run_print execution_id (print as Print {exec_id, print_process, ...}) = if ignore_process print_process then () else if parallel_print print then fork_print execution_id [] print else run_process execution_id exec_id print_process; in fun exec execution_id (eval, prints) = (run_eval execution_id eval; List.app (run_print execution_id) prints); fun exec_parallel_prints execution_id deps (exec as (Eval {eval_process, ...}, prints)) = if Lazy.is_finished eval_process then (List.app (fork_print execution_id deps) prints; NONE) else SOME exec; end; end; diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala +++ b/src/Pure/PIDE/command.scala @@ -1,579 +1,581 @@ /* Title: Pure/PIDE/command.scala Author: Fabian Immler, TU Munich Author: Makarius Prover commands with accumulated results from execution. */ package isabelle import scala.collection.mutable import scala.collection.immutable.SortedMap object Command { type Edit = (Option[Command], Option[Command]) sealed case class Blob( name: Document.Node.Name, + src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) type Blobs_Info = (List[Exn.Result[Blob]], Int) val no_blobs: Blobs_Info = (Nil, -1) /** accumulated results from prover **/ /* results */ object Results { type Entry = (Long, XML.Tree) val empty: Results = new Results(SortedMap.empty) def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _) def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Tree]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) def get(serial: Long): Option[XML.Tree] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = if (defined(entry._1)) this else new Results(rep + entry) def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Results => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Results(", ", ", ")") } /* exports */ object Exports { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) def merge(args: TraversableOnce[Exports]): Exports = (empty /: args)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) { def is_empty: Boolean = rep.isEmpty def iterator: Iterator[Exports.Entry] = rep.iterator def + (entry: Exports.Entry): Exports = if (rep.isDefinedAt(entry._1)) this else new Exports(rep + entry) def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other else (this /: other.iterator)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Exports => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Exports(", ", ", ")") } /* markups */ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { val empty: Markups = new Markups(Map.empty) def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _) } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) { def is_empty: Boolean = rep.isEmpty def apply(index: Markup_Index): Markup_Tree = rep.getOrElse(index, Markup_Tree.empty) def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) def + (entry: (Markup_Index, Markup_Tree)): Markups = { val (index, tree) = entry new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) } def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other else (this /: other.rep.iterator)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Markups => rep == other.rep case _ => false } override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") } /* state */ object State { def get_result(states: List[State], serial: Long): Option[XML.Tree] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) tree @ XML.Elem(_, body) <- get_result(states, serial) if body.nonEmpty } yield (serial -> tree) def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) def merge_exports(states: List[State]): Exports = Exports.merge(states.map(_.exports)) def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) def merge_markup(states: List[State], index: Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(states), merge_markups(states)) } sealed case class State( command: Command, status: List[Markup] = Nil, results: Results = Results.empty, exports: Exports = Exports.empty, markups: Markups = Markups.empty) { def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) lazy val maybe_consolidated: Boolean = { var touched = false var forks = 0 var runs = 0 for (markup <- status) { markup.name match { case Markup.FORKED => touched = true; forks += 1 case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 case _ => } } touched && forks == 0 && runs == 0 } lazy val document_status: Document_Status.Command_Status = { val warnings = if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = if (results.iterator.exists(p => Protocol.is_error(p._2))) List(Markup(Markup.ERROR, Nil)) else Nil Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) } def markup(index: Markup_Index): Markup_Tree = markups(index) def redirect(other_command: Command): Option[State] = { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = copy(status = st :: status) private def add_result(entry: Results.Entry): State = copy(results = results + entry) def add_export(entry: Exports.Entry): Option[State] = if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) else None private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) markups.add(Markup_Index(true, chunk_name), m) else markups copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def accumulate( self_id: Document_ID.Generic => Boolean, other_id: Document_ID.Generic => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem, xml_cache: XML.Cache): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => if (command.span.is_theory) this else { (this /: msgs)((state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => state. add_status(markup). add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) case _ => Output.warning("Ignored status message: " + msg) state }) } case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => (this /: msgs)((state, msg) => { def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { case XML.Elem(Markup(name, atts1), args) => val atts = atts1 ::: atts0 command.reported_position(atts) match { case Some((id, chunk_name)) => val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id) else None (target, atts) match { case (Some((target_name, target_chunk)), Position.Range(symbol_range)) => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = atts.filterNot(Markup.position_property) val elem = xml_cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state } case _ => // silently ignore excessive reports state } case _ => bad(); state } case _ => bad(); state } }) case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => val markup_message = xml_cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) val message_markup = xml_cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) var st = add_result(i -> markup_message) if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator range <- command.message_positions(self_id, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st case _ => Output.warning("Ignored message without serial number: " + message) this } } } /** static content **/ /* make commands */ def apply( id: Document_ID.Command, node_name: Document.Node.Name, blobs_info: Blobs_Info, span: Command_Span.Span): Command = { val (source, span1) = span.compact_source new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty) def unparsed( source: String, theory: Boolean = false, id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, results: Results = Results.empty, markups: Markups = Markups.empty): Command = { val (source1, span1) = Command_Span.unparsed(source, theory).compact_source new Command(id, node_name, no_blobs, span1, source1, results, markups) } def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = unparsed(XML.content(body), id = id, results = results, markups = Markups.init(Markup_Tree.from_XML(body))) /* perspective */ object Perspective { val empty: Perspective = Perspective(Nil) } sealed case class Perspective(commands: List[Command]) // visible commands in canonical order { def is_empty: Boolean = commands.isEmpty def same(that: Perspective): Boolean = { val cmds1 = this.commands val cmds2 = that.commands require(!cmds1.exists(_.is_undefined)) require(!cmds2.exists(_.is_undefined)) cmds1.length == cmds2.length && (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) } } /* blobs: inlined errors and auxiliary files */ def blobs_info( resources: Resources, syntax: Outer_Syntax, get_blob: Document.Node.Name => Option[Document.Blob], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span): Blobs_Info = { span.name match { // inlined errors case Thy_Header.THEORY => val reader = Scan.char_reader(Token.implode(span.content)) val imports_pos = resources.check_thy_reader(node_name, reader).imports_pos val raw_imports = try { val read_imports = Thy_Header.read(reader, Token.Pos.none).imports if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case exn: Throwable => List.fill(imports_pos.length)("") } val errors = for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) } yield { val completion = if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil val msg = "Bad theory import " + Markup.Path(import_name.node).markup(quote(import_name.toString)) + Position.here(pos) + Completion.report_theories(pos, completion) Exn.Exn[Command.Blob](ERROR(msg)) } (errors, -1) // auxiliary files case _ => val (files, index) = span.loaded_files(syntax) val blobs = files.map(file => (Exn.capture { - val name = Document.Node.Name(resources.append(node_name, Path.explode(file))) + val src_path = Path.explode(file) + val name = Document.Node.Name(resources.append(node_name, src_path)) val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk)) - Blob(name, content) + Blob(name, src_path, content) }).user_error) (blobs, index) } } } final class Command private( val id: Document_ID.Command, val node_name: Document.Node.Name, val blobs_info: Command.Blobs_Info, val span: Command_Span.Span, val source: String, val init_results: Command.Results, val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString /* classification */ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY /* blobs */ def blobs: List[Exn.Result[Command.Blob]] = blobs_info._1 def blobs_index: Int = blobs_info._2 def blobs_ok: Boolean = blobs.forall({ case Exn.Res(_) => true case _ => false }) def blobs_names: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs) yield blob.name def blobs_undefined: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest) def blobs_changed(doc_blobs: Document.Blobs): Boolean = blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false }) /* source chunks */ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content) yield Symbol.Text_Chunk.File(blob.name.node) -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range val core_range: Text.Range = Text.Range(0, (length /: span.content.reverse.iterator.takeWhile(_.is_ignored))(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) /* reported positions */ def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] = pos match { case Position.Id(id) => val chunk_name = pos match { case Position.File(name) if name != node_name.node => Symbol.Text_Chunk.File(name) case _ => Symbol.Text_Chunk.Default } Some((id, chunk_name)) case _ => None } def message_positions( self_id: Document_ID.Generic => Boolean, chunk_name: Symbol.Text_Chunk.Name, chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = reported_position(props) match { case Some((id, name)) if self_id(id) && name == chunk_name => val opt_range = Position.Range.unapply(props) orElse { if (name == Symbol.Text_Chunk.Default) Position.Range.unapply(span.position) else None } opt_range match { case Some(symbol_range) => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set } case None => set } case _ => set } def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = t match { case XML.Wrapped_Elem(Markup(name, props), _, body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Elem(Markup(name, props), body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Text(_) => set } val set = tree(Set.empty, message) if (set.isEmpty) elem(message.markup.properties, set) else set } /* accumulated results */ val init_state: Command.State = Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } diff --git a/src/Pure/PIDE/document.ML b/src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML +++ b/src/Pure/PIDE/document.ML @@ -1,895 +1,895 @@ (* Title: Pure/PIDE/document.ML Author: Makarius Document as collection of named nodes, each consisting of an editable list of commands, associated with asynchronous execution process. *) signature DOCUMENT = sig val timing: bool Unsynchronized.ref type node_header = {master: string, header: Thy_Header.header, errors: string list} type overlay = Document_ID.command * (string * string list) datatype node_edit = Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | Perspective of bool * Document_ID.command list * overlay list type edit = string * node_edit type state val init_state: state val define_blob: string -> string -> state -> state - type blob_digest = (string * string option) Exn.result + type blob_digest = {file_node: string, src_path: Path.T, digest: string option} Exn.result type command = {command_id: Document_ID.command, name: string, blobs_digests: blob_digest list, blobs_index: int, tokens: ((int * int) * string) list} val define_command: command -> state -> state val command_exec: state -> string -> Document_ID.command -> Command.exec option val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state val update: Document_ID.version -> Document_ID.version -> edit list -> string list -> state -> string list * Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state val change_state: (state -> state) -> unit end; structure Document: DOCUMENT = struct val timing = Unsynchronized.ref false; fun timeit msg e = cond_timeit (! timing) msg e; (** document structure **) fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); type node_header = {master: string, header: Thy_Header.header, errors: string list}; type perspective = {required: bool, (*required node*) visible: Inttab.set, (*visible commands*) visible_last: Document_ID.command option, (*last visible command*) overlays: (string * string list) list Inttab.table}; (*command id -> print functions with args*) structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); abstype node = Node of {header: node_header, (*master directory, theory header, errors*) keywords: Keyword.keywords option, (*outer syntax keywords*) perspective: perspective, (*command perspective*) entries: Command.exec option Entries.T, (*command entries with executions*) result: (Document_ID.command * Command.eval) option, (*result of last execution*) consolidated: unit lazy} (*consolidated status of eval forks*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with fun make_node (header, keywords, perspective, entries, result, consolidated) = Node {header = header, keywords = keywords, perspective = perspective, entries = entries, result = result, consolidated = consolidated}; fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) = make_node (f (header, keywords, perspective, entries, result, consolidated)); fun make_perspective (required, command_ids, overlays) : perspective = {required = required, visible = Inttab.make_set command_ids, visible_last = try List.last command_ids, overlays = Inttab.make_list overlays}; val no_header: node_header = {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []}; val no_perspective = make_perspective (false, [], []); val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ()); fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) = not required andalso Inttab.is_empty visible andalso is_none visible_last andalso Inttab.is_empty overlays; fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) = header = no_header andalso is_none keywords andalso is_no_perspective perspective andalso Entries.is_empty entries andalso is_none result andalso Lazy.is_finished consolidated; (* basic components *) fun master_directory (Node {header = {master, ...}, ...}) = (case try Url.explode master of SOME (Url.File path) => path | _ => Path.current); fun set_header master header errors = map_node (fn (_, keywords, perspective, entries, result, consolidated) => ({master = master, header = header, errors = errors}, keywords, perspective, entries, result, consolidated)); fun get_header (Node {header, ...}) = header; fun set_keywords keywords = map_node (fn (header, _, perspective, entries, result, consolidated) => (header, keywords, perspective, entries, result, consolidated)); fun get_keywords (Node {keywords, ...}) = keywords; fun read_header node span = let val {header, errors, ...} = get_header node; val _ = if null errors then () else cat_lines errors |> (case Position.get_id (Position.thread_data ()) of NONE => I | SOME id => Protocol_Message.command_positions_yxml id) |> error; val {name = (name, _), imports, ...} = header; val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens Position.none span; val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports; in Thy_Header.make (name, pos) imports'' keywords end; fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective args = map_node (fn (header, keywords, _, entries, result, consolidated) => (header, keywords, make_perspective args, entries, result, consolidated)); val required_node = #required o get_perspective; val visible_command = Inttab.defined o #visible o get_perspective; val visible_last = #visible_last o get_perspective; val visible_node = is_some o visible_last val overlays = Inttab.lookup_list o #overlays o get_perspective; fun map_entries f = map_node (fn (header, keywords, perspective, entries, result, consolidated) => (header, keywords, perspective, f entries, result, consolidated)); fun get_entries (Node {entries, ...}) = entries; fun iterate_entries f = Entries.iterate NONE f o get_entries; fun iterate_entries_after start f (Node {entries, ...}) = (case Entries.get_after entries start of NONE => I | SOME id => Entries.iterate (SOME id) f entries); fun get_result (Node {result, ...}) = result; fun set_result result = map_node (fn (header, keywords, perspective, entries, _, consolidated) => (header, keywords, perspective, entries, result, consolidated)); fun pending_result node = (case get_result node of SOME (_, eval) => not (Command.eval_finished eval) | NONE => false); fun finished_result node = (case get_result node of SOME (_, eval) => Command.eval_finished eval | NONE => false); fun finished_result_theory node = if finished_result node then let val (result_id, eval) = the (get_result node); val st = Command.eval_result_state eval; in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end else NONE; val reset_consolidated = map_node (fn (header, keywords, perspective, entries, result, _) => (header, keywords, perspective, entries, result, Lazy.lazy I)); fun commit_consolidated (Node {consolidated, ...}) = (Lazy.force consolidated; Output.status [Markup.markup_only Markup.consolidated]); fun consolidated_node (Node {consolidated, ...}) = Lazy.is_finished consolidated; fun could_consolidate node = not (consolidated_node node) andalso is_some (finished_result_theory node); fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; fun default_node name = String_Graph.default_node (name, empty_node); fun update_node name f = default_node name #> String_Graph.map_node name f; (* node edits and associated executions *) type overlay = Document_ID.command * (string * string list); datatype node_edit = Edits of (Document_ID.command option * Document_ID.command option) list | Deps of node_header | Perspective of bool * Document_ID.command list * overlay list; type edit = string * node_edit; val after_entry = Entries.get_after o get_entries; fun lookup_entry node id = (case Entries.lookup (get_entries node) id of NONE => NONE | SOME (exec, _) => exec); fun the_entry node id = (case Entries.lookup (get_entries node) id of NONE => err_undef "command entry" id | SOME (exec, _) => exec); fun assign_entry (command_id, exec) node = if is_none (Entries.lookup (get_entries node) command_id) then node else map_entries (Entries.update (command_id, exec)) node; fun reset_after id entries = (case Entries.get_after entries id of NONE => entries | SOME next => Entries.update (next, NONE) entries); val edit_node = map_entries o fold (fn (id, SOME id2) => Entries.insert_after id (id2, NONE) | (id, NONE) => Entries.delete_after id #> reset_after id); (* version operations *) val empty_version = Version String_Graph.empty; fun nodes_of (Version nodes) = nodes; val node_of = get_node o nodes_of; fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); fun edit_nodes (name, node_edit) (Version nodes) = Version (case node_edit of Edits edits => update_node name (edit_node edits) nodes | Deps {master, header, errors} => let val imports = map fst (#imports header); val nodes1 = nodes |> default_node name |> fold default_node imports; val nodes2 = nodes1 |> String_Graph.Keys.fold (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name); val (nodes3, errors1) = (String_Graph.add_deps_acyclic (name, imports) nodes2, errors) handle String_Graph.CYCLES cs => (nodes2, errors @ map cycle_msg cs); in String_Graph.map_node name (set_header master header errors1) nodes3 end | Perspective perspective => update_node name (set_perspective perspective) nodes); fun update_keywords name nodes = nodes |> String_Graph.map_node name (fn node => if is_empty_node node then node else let val {master, header, errors} = get_header node; val imports_keywords = map_filter (get_keywords o get_node nodes o #1) (#imports header); val keywords = Library.foldl Keyword.merge_keywords (Session.get_keywords (), imports_keywords); val (keywords', errors') = (Keyword.add_keywords (#keywords header) keywords, errors) handle ERROR msg => (keywords, if member (op =) errors msg then errors else errors @ [msg]); in node |> set_header master header errors' |> set_keywords (SOME keywords') end); fun edit_keywords edits (Version nodes) = Version (fold update_keywords (String_Graph.all_succs nodes (map_filter (fn (a, Deps _) => SOME a | _ => NONE) edits)) nodes); fun suppressed_node (nodes: node String_Graph.T) (name, node) = String_Graph.is_maximal nodes name andalso is_empty_node node; fun put_node (name, node) (Version nodes) = let val nodes1 = update_node name (K node) nodes; val nodes2 = if suppressed_node nodes1 (name, node) then String_Graph.del_node name nodes1 else nodes1; in Version nodes2 end; end; (** main state -- document structure and execution process **) -type blob_digest = (string * string option) Exn.result; (*file node name, raw digest*) +type blob_digest = {file_node: string, src_path: Path.T, digest: string option} Exn.result; type execution = {version_id: Document_ID.version, (*static version id*) execution_id: Document_ID.execution, (*dynamic execution id*) delay_request: unit future, (*pending event timer request*) parallel_prints: Command.exec list}; (*parallel prints for early execution*) val no_execution: execution = {version_id = Document_ID.none, execution_id = Document_ID.none, delay_request = Future.value (), parallel_prints = []}; fun new_execution version_id delay_request parallel_prints : execution = {version_id = version_id, execution_id = Execution.start (), delay_request = delay_request, parallel_prints = parallel_prints}; abstype state = State of {versions: version Inttab.table, (*version id -> document content*) blobs: (SHA1.digest * string list) Symtab.table, (*raw digest -> digest, lines*) commands: (string * blob_digest list * int * Token.T list lazy) Inttab.table, (*command id -> name, inlined files, token index of files, command span*) execution: execution} (*current execution process*) with fun make_state (versions, blobs, commands, execution) = State {versions = versions, blobs = blobs, commands = commands, execution = execution}; fun map_state f (State {versions, blobs, commands, execution}) = make_state (f (versions, blobs, commands, execution)); val init_state = make_state (Inttab.make [(Document_ID.none, empty_version)], Symtab.empty, Inttab.empty, no_execution); (* document versions *) fun parallel_prints_node node = iterate_entries (fn (_, opt_exec) => fn rev_result => (case opt_exec of SOME (eval, prints) => (case filter Command.parallel_print prints of [] => SOME rev_result | prints' => SOME ((eval, prints') :: rev_result)) | NONE => NONE)) node [] |> rev; fun define_version version_id version assigned_nodes = map_state (fn (versions, blobs, commands, {delay_request, ...}) => let val version' = fold put_node assigned_nodes version; val versions' = Inttab.update_new (version_id, version') versions handle Inttab.DUP dup => err_dup "document version" dup; val parallel_prints = maps (parallel_prints_node o #2) assigned_nodes; val execution' = new_execution version_id delay_request parallel_prints; in (versions', blobs, commands, execution') end); fun the_version (State {versions, ...}) version_id = (case Inttab.lookup versions version_id of NONE => err_undef "document version" version_id | SOME version => version); fun delete_version version_id versions = Inttab.delete version_id versions handle Inttab.UNDEF _ => err_undef "document version" version_id; (* inlined files *) fun define_blob digest text = map_state (fn (versions, blobs, commands, execution) => let val blobs' = Symtab.update (digest, (SHA1.fake digest, split_lines text)) blobs in (versions, blobs', commands, execution) end); fun the_blob (State {blobs, ...}) digest = (case Symtab.lookup blobs digest of NONE => error ("Undefined blob: " ^ digest) | SOME content => content); fun resolve_blob state (blob_digest: blob_digest) = - blob_digest |> Exn.map_res (fn (file_node, raw_digest) => - (file_node, Option.map (the_blob state) raw_digest)); + blob_digest |> Exn.map_res (fn {file_node, src_path, digest} => + {file_node = file_node, src_path = src_path, content = Option.map (the_blob state) digest}); fun blob_reports pos (blob_digest: blob_digest) = - (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []); + (case blob_digest of Exn.Res {file_node, ...} => [(pos, Markup.path file_node)] | _ => []); (* commands *) type command = {command_id: Document_ID.command, name: string, blobs_digests: blob_digest list, blobs_index: int, tokens: ((int * int) * string) list}; fun define_command {command_id, name, blobs_digests, blobs_index, tokens} = map_state (fn (versions, blobs, commands, execution) => let val id = Document_ID.print command_id; val span = Lazy.lazy_name "Document.define_command" (fn () => Position.setmp_thread_data (Position.id_only id) (fn () => let val (tokens, _) = fold_map Token.make tokens (Position.id id); val _ = if blobs_index < 0 then (*inlined errors*) map_filter Exn.get_exn blobs_digests |> List.app (Output.error_message o Runtime.exn_message) else (*auxiliary files*) let val pos = Token.pos_of (nth tokens blobs_index) in Position.reports (maps (blob_reports pos) blobs_digests) end; in tokens end) ()); val commands' = Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands handle Inttab.DUP dup => err_dup "command" dup; in (versions, blobs, commands', execution) end); fun the_command (State {commands, ...}) command_id = (case Inttab.lookup commands command_id of NONE => err_undef "command" command_id | SOME command => command); val the_command_name = #1 oo the_command; (* execution *) fun get_execution (State {execution, ...}) = execution; fun get_execution_version state = the_version state (#version_id (get_execution state)); fun command_exec state node_name command_id = let val version = get_execution_version state; val node = get_node (nodes_of version) node_name; in the_entry node command_id end; end; (* remove_versions *) fun remove_versions version_ids state = state |> map_state (fn (versions, _, _, execution) => let val _ = member (op =) version_ids (#version_id execution) andalso error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution)); val versions' = fold delete_version version_ids versions; val commands' = (versions', Inttab.empty) |-> Inttab.fold (fn (_, version) => nodes_of version |> String_Graph.fold (fn (_, (node, _)) => node |> iterate_entries (fn ((_, command_id), _) => SOME o Inttab.insert (K true) (command_id, the_command state command_id)))); val blobs' = (commands', Symtab.empty) |-> Inttab.fold (fn (_, (_, blobs, _, _)) => blobs |> - fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I)); + fold (fn Exn.Res {digest = SOME b, ...} => Symtab.update (b, the_blob state b) | _ => I)); in (versions', blobs', commands', execution) end); (* document execution *) fun make_required nodes = let fun all_preds P = String_Graph.fold (fn (a, (node, _)) => P node ? cons a) nodes [] |> String_Graph.all_preds nodes |> Symtab.make_set; val all_visible = all_preds visible_node; val all_required = all_preds required_node; in Symtab.fold (fn (a, ()) => exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? Symtab.update (a, ())) all_visible all_required end; fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) => timeit "Document.start_execution" (fn () => let val {version_id, execution_id, delay_request, parallel_prints} = execution; val delay = seconds (Options.default_real "editor_execution_delay"); val _ = Future.cancel delay_request; val delay_request' = Event_Timer.future {physical = true} (Time.now () + delay); val delay = Future.task_of delay_request'; val parallel_prints' = parallel_prints |> map_filter (Command.exec_parallel_prints execution_id [delay]); fun finished_import (name, (node, _)) = finished_result node orelse is_some (Thy_Info.lookup_theory name); val nodes = nodes_of (the_version state version_id); val required = make_required nodes; val _ = nodes |> String_Graph.schedule (fn deps => fn (name, node) => if Symtab.defined required name orelse visible_node node orelse pending_result node then let val future = (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group NONE), deps = delay :: Execution.active_tasks name @ maps (the_list o #2 o #2) deps, pri = 0, interrupts = false} (fn () => (Execution.worker_task_active true name; if forall finished_import deps then iterate_entries (fn (_, opt_exec) => fn () => (case opt_exec of SOME exec => if Execution.is_running execution_id then SOME (Command.exec execution_id exec) else NONE | NONE => NONE)) node () else (); Execution.worker_task_active false name) handle exn => (Output.system_message (Runtime.exn_message exn); Execution.worker_task_active false name; Exn.reraise exn)); in (node, SOME (Future.task_of future)) end else (node, NONE)); val execution' = {version_id = version_id, execution_id = execution_id, delay_request = delay_request', parallel_prints = parallel_prints'}; in (versions, blobs, commands, execution') end)); (** document update **) (* exec state assignment *) type assign_update = Command.exec option Inttab.table; (*command id -> exec*) val assign_update_empty: assign_update = Inttab.empty; fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab; fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; fun assign_update_new upd (tab: assign_update) = Inttab.update_new upd tab handle Inttab.DUP dup => err_dup "exec state assignment" dup; fun assign_update_result (tab: assign_update) = Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab []; (* update *) local fun init_theory deps node span = let val master_dir = master_directory node; val header = read_header node span; val imports = #imports header; fun maybe_eval_result eval = Command.eval_result_state eval handle Fail _ => Toplevel.init_toplevel (); fun maybe_end_theory pos st = SOME (Toplevel.end_theory pos st) handle ERROR msg => (Output.error_message msg; NONE); val parents_reports = imports |> map_filter (fn (import, pos) => (case Thy_Info.lookup_theory import of NONE => maybe_end_theory pos (case get_result (snd (the (AList.lookup (op =) deps import))) of NONE => Toplevel.init_toplevel () | SOME (_, eval) => maybe_eval_result eval) | some => some) |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))); val parents = if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports; val _ = List.app (fn (thy, r) => Context_Position.reports_global thy [r]) parents_reports; val thy = Resources.begin_theory master_dir header parents; val _ = Output.status [Markup.markup_only Markup.initialized]; in thy end; fun check_root_theory node = let val master_dir = master_directory node; val header = #header (get_header node); val header_name = #1 (#name header); val parent = if header_name = Sessions.root_name then SOME (Thy_Info.get_theory Sessions.theory_name) else if member (op =) Thy_Header.ml_roots header_name then SOME (Thy_Info.get_theory Thy_Header.ml_bootstrapN) else NONE; in parent |> Option.map (fn thy => Resources.begin_theory master_dir header [thy]) end; fun check_theory full name node = is_some (Thy_Info.lookup_theory name) orelse null (#errors (get_header node)) andalso (not full orelse is_some (get_result node)); fun last_common keywords state node_required node0 node = let fun update_flags prev (visible, initial) = let val visible' = visible andalso prev <> visible_last node; val initial' = initial andalso (case prev of NONE => true | SOME command_id => the_command_name state command_id <> Thy_Header.theoryN); in (visible', initial') end; fun get_common ((prev, command_id), opt_exec) (_, ok, flags, assign_update) = if ok then let val flags' as (visible', _) = update_flags prev flags; val ok' = (case (lookup_entry node0 command_id, opt_exec) of (SOME (eval0, _), SOME (eval, _)) => Command.eval_eq (eval0, eval) andalso (visible' orelse node_required orelse Command.eval_running eval) | _ => false); val assign_update' = assign_update |> ok' ? (case opt_exec of SOME (eval, prints) => let val command_visible = visible_command node command_id; val command_overlays = overlays node command_id; val command_name = the_command_name state command_id; in (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 | NONE => I); in SOME (prev, ok', flags', assign_update') end else NONE; val (common, ok, flags, assign_update') = iterate_entries get_common node (NONE, true, (true, true), assign_update_empty); val (common', flags') = if ok then let val last = Entries.get_after (get_entries node) common in (last, update_flags last flags) end else (common, flags); in (assign_update', common', flags') end; fun illegal_init _ = error "Illegal theory header"; 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 val command_visible = visible_command node command_id'; val command_overlays = overlays node command_id'; val (command_name, blob_digests, blobs_index, span0) = the_command state command_id'; val blobs = map (resolve_blob state) blob_digests; val span = Lazy.force span0; val eval' = Command.eval keywords (master_directory node) (fn () => the_default illegal_init init span) (blobs, blobs_index) command_id' span (#1 (#2 command_exec)); 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 command_name = Thy_Header.theoryN then NONE else init; in SOME (assign_update', (command_id', exec'), init') end; fun removed_execs node0 (command_id, exec_ids) = subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); fun print_consolidation options the_command_span node_name (assign_update, node) = (case finished_result_theory node of SOME (result_id, thy) => let val active_tasks = (node, false) |-> iterate_entries (fn (_, opt_exec) => fn active => if active then NONE else (case opt_exec of NONE => NONE | SOME (eval, _) => SOME (not (null (Execution.snapshot [Command.eval_exec_id eval]))))); in if not active_tasks then let val consolidation = if Options.bool options "editor_presentation" then let val (_, offsets, rev_segments) = iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => (case opt_exec of SOME (eval, _) => let val command_id = Command.eval_command_id eval; val span = the_command_span command_id; val exec_id = Command.eval_exec_id eval; val tr = Command.eval_result_command eval; val st' = Command.eval_result_state eval; val offset' = offset + the_default 0 (Command_Span.symbol_length span); val offsets' = offsets |> Inttab.update (command_id, offset) |> Inttab.update (exec_id, offset); val segments' = (span, tr, st') :: segments; in SOME (offset', offsets', segments') end | NONE => NONE)) node (0, Inttab.empty, []); val adjust = Inttab.lookup offsets; val segments = rev rev_segments |> map (fn (span, tr, st') => {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); val presentation_context: Thy_Info.presentation_context = {options = options, file_pos = Position.file node_name, adjust_pos = Position.adjust_offsets adjust, segments = segments}; in fn _ => let val _ = Output.status [Markup.markup_only Markup.consolidating]; val res = Exn.capture (Thy_Info.apply_presentation presentation_context) thy; val _ = commit_consolidated node; in Exn.release res end end else fn _ => commit_consolidated node; val result_entry = (case lookup_entry node result_id of NONE => err_undef "result command entry" result_id | SOME (eval, prints) => let val print = eval |> Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = K consolidation}; in (result_id, SOME (eval, print :: prints)) end); val assign_update' = assign_update |> assign_update_change result_entry; val node' = node |> assign_entry result_entry; in (assign_update', node') end else (assign_update, node) end | NONE => (assign_update, node)); in fun update old_version_id new_version_id edits consolidate state = Runtime.exn_trace_system (fn () => let val options = Options.default (); val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state; val old_version = the_version state old_version_id; val new_version = timeit "Document.edit_nodes" (fn () => old_version |> fold edit_nodes edits |> edit_keywords edits); val consolidate = Symtab.defined (Symtab.make_set consolidate); val nodes = nodes_of new_version; val required = make_required nodes; val required0 = make_required (nodes_of old_version); val edited = fold (fn (name, _) => Symtab.update (name, ())) edits Symtab.empty; val updated = timeit "Document.update" (fn () => nodes |> String_Graph.schedule (fn deps => fn (name, node) => (singleton o Future.forks) {name = "Document.update", group = NONE, deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} (fn () => timeit ("Document.update " ^ name) (fn () => Runtime.exn_trace_system (fn () => let val root_theory = check_root_theory node; val keywords = the_default (Session.get_keywords ()) (get_keywords node); val maybe_consolidate = consolidate name andalso could_consolidate node; 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; in if Symtab.defined edited name orelse maybe_consolidate orelse visible_node node orelse imports_result_changed orelse Symtab.defined required0 name <> node_required then let val node0 = node_of old_version name; val init = init_theory imports node; val proper_init = is_some root_theory orelse check_theory false name node andalso forall (fn (name, (_, node)) => check_theory true name node) imports; val (print_execs, common, (still_visible, initial)) = if imports_result_changed then (assign_update_empty, NONE, (true, true)) else last_common keywords state node_required node0 node; val common_command_exec = (case common of SOME id => (id, the_default Command.no_exec (the_entry node id)) | NONE => (Document_ID.none, Command.init_exec root_theory)); val (updated_execs, (command_id', exec'), _) = (print_execs, common_command_exec, if initial then SOME init else NONE) |> (still_visible orelse node_required) ? iterate_entries_after common (fn ((prev, id), _) => fn res => if not node_required andalso prev = visible_last node then NONE else new_exec keywords state node proper_init id res) node; val assign_update = (node0, updated_execs) |-> iterate_entries_after common (fn ((_, command_id0), exec0) => fn res => if is_none exec0 then NONE else if assign_update_defined updated_execs command_id0 then SOME res else SOME (assign_update_new (command_id0, NONE) res)); val last_exec = if command_id' = Document_ID.none then NONE else SOME command_id'; val result = if is_none last_exec orelse is_some (after_entry node last_exec) then NONE else SOME (command_id', #1 exec'); val result_changed = not (eq_option (Command.eval_eq o apply2 #2) (get_result node0, result)); val (assign_update', node') = node |> assign_update_apply assign_update |> set_result result |> result_changed ? reset_consolidated |> pair assign_update |> (not result_changed andalso maybe_consolidate) ? print_consolidation options the_command_span name; val assign_result = assign_update_result assign_update'; val removed = maps (removed_execs node0) assign_result; val _ = List.app Execution.cancel removed; val assigned_node = SOME (name, node'); in ((removed, assign_result, assigned_node, result_changed), node') end else (([], [], NONE, false), node) end)))) |> Future.joins |> map #1); val removed = maps #1 updated; val assign_result = maps #2 updated; val assigned_nodes = map_filter #3 updated; val state' = state |> define_version new_version_id new_version assigned_nodes; in (Symtab.keys edited, removed, assign_result, state') end); end; (** global state **) val global_state = Synchronized.var "Document.global_state" init_state; fun state () = Synchronized.value global_state; val change_state = Synchronized.change global_state; end; diff --git a/src/Pure/PIDE/protocol.ML b/src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML +++ b/src/Pure/PIDE/protocol.ML @@ -1,170 +1,172 @@ (* Title: Pure/PIDE/protocol.ML Author: Makarius Protocol message formats for interactive proof documents. *) structure Protocol: sig end = struct val _ = Isabelle_Process.protocol_command "Prover.echo" (fn args => List.app writeln args); val _ = Isabelle_Process.protocol_command "Prover.stop" (fn rc :: msgs => (List.app Output.system_message msgs; raise Isabelle_Process.STOP (Value.parse_int rc))); val _ = Isabelle_Process.protocol_command "Prover.options" (fn [options_yxml] => (Options.set_default (Options.decode (YXML.parse_body options_yxml)); Isabelle_Process.init_options_interactive ())); val _ = Isabelle_Process.protocol_command "Prover.init_session" (fn [yxml] => Resources.init_session_yxml yxml); val _ = Isabelle_Process.protocol_command "Document.define_blob" (fn [digest, content] => Document.change_state (Document.define_blob digest content)); fun decode_command id name blobs_xml toks_xml sources : Document.command = let open XML.Decode; val (blobs_digests, blobs_index) = blobs_xml |> let val message = YXML.string_of_body o Protocol_Message.command_positions id; + val blob = + triple string string (option string) + #> (fn (a, b, c) => {file_node = a, src_path = Path.explode b, digest = c}); in pair (list (variant - [fn ([], a) => Exn.Res (pair string (option string) a), + [fn ([], a) => Exn.Res (blob a), fn ([], a) => Exn.Exn (ERROR (message a))])) int end; val toks = list (pair int int) toks_xml; in {command_id = Document_ID.parse id, name = name, blobs_digests = blobs_digests, blobs_index = blobs_index, tokens = toks ~~ sources} end; fun commands_accepted ids = Output.protocol_message Markup.commands_accepted [XML.Text (space_implode "," ids)]; val _ = Isabelle_Process.protocol_command "Document.define_command" (fn id :: name :: blobs :: toks :: sources => let val command = decode_command id name (YXML.parse_body blobs) (YXML.parse_body toks) sources; val _ = Document.change_state (Document.define_command command); in commands_accepted [id] end); val _ = Isabelle_Process.protocol_command "Document.define_commands" (fn args => let fun decode arg = let open XML.Decode; val (id, (name, (blobs_xml, (toks_xml, sources)))) = pair string (pair string (pair I (pair I (list string)))) (YXML.parse_body arg); in decode_command id name blobs_xml toks_xml sources end; val commands = map decode args; val _ = Document.change_state (fold Document.define_command commands); in commands_accepted (map (Value.print_int o #command_id) commands) end); val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" (fn [] => Execution.discontinue ()); val _ = Isabelle_Process.protocol_command "Document.cancel_exec" (fn [exec_id] => Execution.cancel (Document_ID.parse exec_id)); val _ = Isabelle_Process.protocol_command "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) (fn old_id_string :: new_id_string :: consolidate_yxml :: edits_yxml => Document.change_state (fn state => let val old_id = Document_ID.parse old_id_string; val new_id = Document_ID.parse new_id_string; val consolidate = YXML.parse_body consolidate_yxml |> let open XML.Decode in list string end; val edits = edits_yxml |> map (YXML.parse_body #> let open XML.Decode in pair string (variant [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => let val (master, (name, (imports, (keywords, errors)))) = pair string (pair string (pair (list string) - (pair (list (pair string - (pair (pair string (list string)) (list string)))) + (pair (list (pair string (pair string (list string)))) (list YXML.string_of_body)))) a; val imports' = map (rpair Position.none) imports; val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; val header = Thy_Header.make (name, Position.none) imports' keywords'; in Document.Deps {master = master, header = header, errors = errors} end, fn (a :: b, c) => Document.Perspective (bool_atom a, map int_atom b, list (pair int (pair string (list string))) c)]) end); val _ = Execution.discontinue (); val (edited, removed, assign_update, state') = Document.update old_id new_id edits consolidate state; val _ = (singleton o Future.forks) {name = "Document.update/remove", group = NONE, deps = Execution.snapshot removed, pri = Task_Queue.urgent_pri + 2, interrupts = false} (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); val _ = Output.protocol_message Markup.assign_update ((new_id, edited, assign_update) |> let open XML.Encode; fun encode_upd (a, bs) = string (space_implode "," (map Value.print_int (a :: bs))); in triple int (list string) (list encode_upd) end); in Document.start_execution state' end))); val _ = Isabelle_Process.protocol_command "Document.remove_versions" (fn [versions_yxml] => Document.change_state (fn state => let val versions = YXML.parse_body versions_yxml |> let open XML.Decode in list int end; val state1 = Document.remove_versions versions state; val _ = Output.protocol_message Markup.removed_versions [XML.Text (versions_yxml)]; in state1 end)); val _ = Isabelle_Process.protocol_command "Document.dialog_result" (fn [serial, result] => Active.dialog_result (Value.parse_int serial) result handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn); val _ = Isabelle_Process.protocol_command "ML_Heap.full_gc" (fn [] => ML_Heap.full_gc ()); val _ = Isabelle_Process.protocol_command "ML_Heap.share_common_data" (fn [] => ML_Heap.share_common_data ()); end; diff --git a/src/Pure/PIDE/protocol.scala b/src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala +++ b/src/Pure/PIDE/protocol.scala @@ -1,429 +1,429 @@ /* Title: Pure/PIDE/protocol.scala Author: Makarius Protocol message formats for interactive proof documents. */ package isabelle object Protocol { /* markers for inlined messages */ val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") val Meta_Info_Marker = Protocol_Message.Marker("meta_info") val Command_Timing_Marker = Protocol_Message.Marker("command_timing") val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing") val Session_Timing_Marker = Protocol_Message.Marker("session_timing") val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics") val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics") val Error_Message_Marker = Protocol_Message.Marker("error_message") /* batch build */ object Loading_Theory { def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] = (props, props, props) match { case (Markup.Name(name), Position.File(file), Position.Id(id)) if Path.is_wellformed(file) => val master_dir = Path.explode(file).dir.implode Some((Document.Node.Name(file, master_dir, name), id)) case _ => None } } /* document editing */ object Commands_Accepted { def unapply(text: String): Option[List[Document_ID.Command]] = try { Some(space_explode(',', text).map(Value.Long.parse)) } catch { case ERROR(_) => None } val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED))) } object Assign_Update { def unapply(text: String) : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = { try { import XML.Decode._ def decode_upd(body: XML.Body): (Long, List[Long]) = space_explode(',', string(body)).map(Value.Long.parse) match { case a :: bs => (a, bs) case _ => throw new XML.XML_Body(body) } Some(triple(long, list(string), list(decode_upd))(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None case _: XML.Error => None } } } object Removed { def unapply(text: String): Option[List[Document_ID.Version]] = try { import XML.Decode._ Some(list(long)(Symbol.decode_yxml(text))) } catch { case ERROR(_) => None case _: XML.Error => None } } /* command timing */ object Command_Timing { def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] = props match { case Markup.Command_Timing(args) => (args, args) match { case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing)) case _ => None } case _ => None } } /* theory timing */ object Theory_Timing { def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = props match { case Markup.Theory_Timing(args) => (args, args) match { case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) case _ => None } case _ => None } } /* result messages */ def is_message(pred: XML.Elem => Boolean, body: XML.Body): Boolean = body match { case List(elem: XML.Elem) => pred(elem) case _ => false } def is_result(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.RESULT, _), _) => true case _ => false } def is_tracing(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.TRACING, _), _) => true case XML.Elem(Markup(Markup.TRACING_MESSAGE, _), _) => true case _ => false } def is_state(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.STATE, _), _) => true case XML.Elem(Markup(Markup.STATE_MESSAGE, _), _) => true case _ => false } def is_information(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.INFORMATION, _), _) => true case XML.Elem(Markup(Markup.INFORMATION_MESSAGE, _), _) => true case _ => false } def is_writeln(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WRITELN, _), _) => true case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true case _ => false } def is_warning(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.WARNING, _), _) => true case XML.Elem(Markup(Markup.WARNING_MESSAGE, _), _) => true case _ => false } def is_legacy(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.LEGACY, _), _) => true case XML.Elem(Markup(Markup.LEGACY_MESSAGE, _), _) => true case _ => false } def is_error(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.ERROR, _), _) => true case XML.Elem(Markup(Markup.ERROR_MESSAGE, _), _) => true case _ => false } def is_inlined(msg: XML.Tree): Boolean = !(is_result(msg) || is_tracing(msg) || is_state(msg)) def is_exported(msg: XML.Tree): Boolean = is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) def message_text(body: XML.Body, margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Pretty.Default_Metric): String = { val text = Pretty.string_of(Protocol_Message.expose_no_reports(body), margin = margin, breakgain = breakgain, metric = metric) if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text) else if (is_message(is_error, body)) Output.error_prefix(text) else text } /* export */ object Export { sealed case class Args( id: Option[String] = None, serial: Long = 0L, theory_name: String, name: String, executable: Boolean = false, compress: Boolean = true, strict: Boolean = true) { def compound_name: String = isabelle.Export.compound_name(theory_name, name) } def unapply(props: Properties.T): Option[Args] = props match { case List( (Markup.FUNCTION, Markup.EXPORT), (Markup.ID, id), (Markup.SERIAL, Value.Long(serial)), (Markup.THEORY_NAME, theory_name), (Markup.NAME, name), (Markup.EXECUTABLE, Value.Boolean(executable)), (Markup.COMPRESS, Value.Boolean(compress)), (Markup.STRICT, Value.Boolean(strict))) => Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict)) case _ => None } } /* breakpoints */ object ML_Breakpoint { def unapply(tree: XML.Tree): Option[Long] = tree match { case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint) case _ => None } } /* dialogs */ object Dialog_Args { def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] = (props, props, props) match { case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) => Some((id, serial, result)) case _ => None } } object Dialog { def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] = tree match { case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) => Some((id, serial, result)) case _ => None } } object Dialog_Result { def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = { val props = Position.Id(id) ::: Markup.Serial(serial) XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result))) } def unapply(tree: XML.Tree): Option[String] = tree match { case XML.Elem(Markup(Markup.RESULT, _), List(XML.Text(result))) => Some(result) case _ => None } } } trait Protocol { /* protocol commands */ def protocol_command_raw(name: String, args: List[Bytes]): Unit def protocol_command_args(name: String, args: List[String]) def protocol_command(name: String, args: String*): Unit /* options */ def options(opts: Options): Unit = protocol_command("Prover.options", Symbol.encode_yxml(opts.encode)) /* resources */ def init_session(resources: Resources): Unit = protocol_command("Prover.init_session", resources.init_session_yxml) /* interned items */ def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit = protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes)) private def encode_command(command: Command): (String, String, String, String, List[String]) = { import XML.Encode._ val blobs_yxml = { val encode_blob: T[Exn.Result[Command.Blob]] = variant(List( - { case Exn.Res(Command.Blob(a, b)) => - (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, + { case Exn.Res(Command.Blob(a, b, c)) => + (Nil, triple(string, string, option(string))( + (a.node, b.implode, c.map(p => p._1.toString)))) }, { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) } val toks_yxml = { val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source)))) Symbol.encode_yxml(list(encode_tok)(command.span.content)) } val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source)) (Document_ID(command.id), Symbol.encode(command.span.name), blobs_yxml, toks_yxml, toks_sources) } def define_command(command: Command) { val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) protocol_command_args( "Document.define_command", command_id :: name :: blobs_yxml :: toks_yxml :: toks_sources) } def define_commands(commands: List[Command]) { protocol_command_args("Document.define_commands", commands.map(command => { import XML.Encode._ val (command_id, name, blobs_yxml, toks_yxml, toks_sources) = encode_command(command) val body = pair(string, pair(string, pair(string, pair(string, list(string)))))( command_id, (name, (blobs_yxml, (toks_yxml, toks_sources)))) YXML.string_of_body(body) })) } def define_commands_bulk(commands: List[Command]) { val (irregular, regular) = commands.partition(command => YXML.detect(command.source)) irregular.foreach(define_command) regular match { case Nil => case List(command) => define_command(command) case _ => define_commands(regular) } } /* execution */ def discontinue_execution(): Unit = protocol_command("Document.discontinue_execution") def cancel_exec(id: Document_ID.Exec): Unit = protocol_command("Document.cancel_exec", Document_ID(id)) /* document versions */ def update(old_id: Document_ID.Version, new_id: Document_ID.Version, edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]) { val consolidate_yxml = { import XML.Encode._ Symbol.encode_yxml(list(string)(consolidate.map(_.node))) } val edits_yxml = { import XML.Encode._ def id: T[Command] = (cmd => long(cmd.id)) def encode_edit(name: Document.Node.Name) : T[Document.Node.Edit[Command.Edit, Command.Perspective]] = variant(List( { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, { case Document.Node.Deps(header) => val master_dir = File.standard_url(name.master_dir) val imports = header.imports.map(_.node) - val keywords = - header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) }) + val keywords = header.keywords.map({ case (a, Keyword.Spec(b, _, c)) => (a, (b, c)) }) (Nil, - pair(string, pair(string, pair(list(string), pair(list(pair(string, - pair(pair(string, list(string)), list(string)))), list(string)))))( + pair(string, pair(string, pair(list(string), + pair(list(pair(string, pair(string, list(string)))), list(string)))))( (master_dir, (name.theory, (imports, (keywords, header.errors)))))) }, { case Document.Node.Perspective(a, b, c) => (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)), list(pair(id, pair(string, list(string))))(c.dest)) })) edits.map({ case (name, edit) => Symbol.encode_yxml(pair(string, encode_edit(name))(name.node, edit)) }) } protocol_command_args("Document.update", Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml) } def remove_versions(versions: List[Document.Version]) { val versions_yxml = { import XML.Encode._ Symbol.encode_yxml(list(long)(versions.map(_.id))) } protocol_command("Document.remove_versions", versions_yxml) } /* dialog via document content */ def dialog_result(serial: Long, result: String): Unit = protocol_command("Document.dialog_result", Value.Long(serial), result) } diff --git a/src/Pure/PIDE/resources.ML b/src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML +++ b/src/Pure/PIDE/resources.ML @@ -1,393 +1,403 @@ (* Title: Pure/PIDE/resources.ML Author: Makarius Resources for theories and auxiliary files. *) signature RESOURCES = sig val default_qualifier: string val init_session: {session_positions: (string * Properties.T) list, session_directories: (string * string) list, session_chapters: (string * string) list, bibtex_entries: (string * string list) list, command_timings: Properties.T list, docs: string list, global_theories: (string * string) list, loaded_theories: string list} -> unit val init_session_yxml: string -> unit val init_session_file: Path.T -> unit val finish_session_base: unit -> unit val global_theory: string -> string option val loaded_theory: string -> bool val check_session: Proof.context -> string * Position.T -> string val session_chapter: string -> string val last_timing: Toplevel.transition -> Time.time val check_doc: Proof.context -> string * Position.T -> string val master_directory: theory -> Path.T val imports_of: theory -> (string * Position.T) list val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val thy_path: Path.T -> Path.T val theory_qualifier: string -> string val theory_bibtex_entries: string -> string list val find_theory_file: string -> Path.T option val import_name: string -> Path.T -> string -> {node_name: Path.T, master_dir: Path.T, theory_name: string} val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} - val parse_files: string -> (theory -> Token.file list) parser + val extensions: string list -> Path.T -> Path.T list + val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser + val parse_file: (theory -> Token.file) parser val provide: Path.T * SHA1.digest -> theory -> theory val provide_file: Token.file -> theory -> theory - val provide_parse_files: string -> (theory -> Token.file list * theory) parser + val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser + val provide_parse_file: (theory -> Token.file * theory) parser val loaded_files_current: theory -> bool val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T end; structure Resources: RESOURCES = struct (* command timings *) type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) val empty_timings: timings = Symtab.empty; fun update_timings props = (case Markup.parse_command_timing_properties props of SOME ({file, offset, name}, time) => Symtab.map_default (file, Inttab.empty) (Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) | NONE => I); fun make_timings command_timings = fold update_timings command_timings empty_timings; fun approximative_id name pos = (case (Position.file_of pos, Position.offset_of pos) of (SOME file, SOME offset) => if name = "" then NONE else SOME {file = file, offset = offset, name = name} | _ => NONE); fun get_timings timings tr = (case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of SOME {file, offset, name} => (case Symtab.lookup timings file of SOME offsets => (case Inttab.lookup offsets offset of SOME (name', time) => if name = name' then SOME time else NONE | NONE => NONE) | NONE => NONE) | NONE => NONE) |> the_default Time.zeroTime; (* session base *) val default_qualifier = "Draft"; type entry = {pos: Position.T, serial: serial}; fun make_entry props : entry = {pos = Position.of_properties props, serial = serial ()}; val empty_session_base = {session_positions = []: (string * entry) list, session_directories = Symtab.empty: Path.T list Symtab.table, session_chapters = Symtab.empty: string Symtab.table, bibtex_entries = Symtab.empty: string list Symtab.table, timings = empty_timings, docs = []: (string * entry) list, global_theories = Symtab.empty: string Symtab.table, loaded_theories = Symtab.empty: unit Symtab.table}; val global_session_base = Synchronized.var "Sessions.base" empty_session_base; fun init_session {session_positions, session_directories, session_chapters, bibtex_entries, command_timings, docs, global_theories, loaded_theories} = Synchronized.change global_session_base (fn _ => {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), session_directories = fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) session_directories Symtab.empty, session_chapters = Symtab.make session_chapters, bibtex_entries = Symtab.make bibtex_entries, timings = make_timings command_timings, docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), global_theories = Symtab.make global_theories, loaded_theories = Symtab.make_set loaded_theories}); fun init_session_yxml yxml = let val (session_positions, (session_directories, (session_chapters, (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories))))))) = YXML.parse_body yxml |> let open XML.Decode in (pair (list (pair string properties)) (pair (list (pair string string)) (pair (list (pair string string)) (pair (list (pair string (list string))) (pair (list properties) (pair (list string) (pair (list (pair string string)) (list string)))))))) end; in init_session {session_positions = session_positions, session_directories = session_directories, session_chapters = session_chapters, bibtex_entries = bibtex_entries, command_timings = command_timings, docs = docs, global_theories = global_theories, loaded_theories = loaded_theories} end; fun init_session_file path = init_session_yxml (File.read path) before File.rm path; fun finish_session_base () = Synchronized.change global_session_base (fn {global_theories, loaded_theories, ...} => {session_positions = [], session_directories = Symtab.empty, session_chapters = Symtab.empty, bibtex_entries = Symtab.empty, timings = empty_timings, docs = [], global_theories = global_theories, loaded_theories = loaded_theories}); fun get_session_base f = f (Synchronized.value global_session_base); fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; fun check_name which kind markup ctxt arg = Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt arg; val check_session = check_name #session_positions "session" (fn (name, {pos, serial}) => Markup.entity Markup.sessionN name |> Markup.properties (Position.entity_properties_of false serial pos)); fun session_chapter name = the_default "Unsorted" (Symtab.lookup (get_session_base #session_chapters) name); fun last_timing tr = get_timings (get_session_base #timings) tr; val check_doc = check_name #docs "documentation" (Markup.doc o #1); (* manage source files *) type files = {master_dir: Path.T, (*master directory of theory source*) imports: (string * Position.T) list, (*source specification of imports*) provided: (Path.T * SHA1.digest) list}; (*source path, digest*) fun make_files (master_dir, imports, provided): files = {master_dir = master_dir, imports = imports, provided = provided}; structure Files = Theory_Data ( type T = files; val empty = make_files (Path.current, [], []); val extend = I; fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = let val provided' = Library.merge (op =) (provided1, provided2) in make_files (master_dir, imports, provided') end ); fun map_files f = Files.map (fn {master_dir, imports, provided} => make_files (f (master_dir, imports, provided))); val master_directory = #master_dir o Files.get; val imports_of = #imports o Files.get; fun begin_theory master_dir {name, imports, keywords} parents = Theory.begin_theory name parents |> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |> Thy_Header.add_keywords keywords; (* theory files *) val thy_path = Path.ext "thy"; fun theory_qualifier theory = (case global_theory theory of SOME qualifier => qualifier | NONE => Long_Name.qualifier theory); fun theory_name qualifier theory = if Long_Name.is_qualified theory orelse is_some (global_theory theory) then theory else Long_Name.qualify qualifier theory; fun theory_bibtex_entries theory = Symtab.lookup_list (get_session_base #bibtex_entries) (theory_qualifier theory); fun find_theory_file thy_name = let val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); val session = theory_qualifier thy_name; val dirs = Symtab.lookup_list (get_session_base #session_directories) session; in dirs |> get_first (fn dir => let val path = dir + thy_file in if File.is_file path then SOME path else NONE end) end; fun make_theory_node node_name theory = {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; fun loaded_theory_node theory = {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; fun import_name qualifier dir s = let val theory = theory_name qualifier (Thy_Header.import_name s); fun theory_node () = make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; in if not (Thy_Header.is_base_name s) then theory_node () else if loaded_theory theory then loaded_theory_node theory else (case find_theory_file theory of SOME node_name => make_theory_node node_name theory | NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) end; fun check_file dir file = File.check_file (File.full_path dir file); fun check_thy dir thy_name = let val thy_base_name = Long_Name.base_name thy_name; val master_file = (case find_theory_file thy_name of SOME path => check_file Path.current path | NONE => check_file dir (thy_path (Path.basic thy_base_name))); val text = File.read master_file; val {name = (name, pos), imports, keywords} = Thy_Header.read (Path.position master_file) text; val _ = thy_base_name <> name andalso error ("Bad theory name " ^ quote name ^ " for file " ^ Path.print (Path.base master_file) ^ Position.here pos); in {master = (master_file, SHA1.digest text), text = text, theory_pos = pos, imports = imports, keywords = keywords} end; (* load files *) -fun parse_files cmd = +fun extensions exts path = map (fn ext => Path.ext ext path) exts; + +fun parse_files make_paths = Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => (case Token.get_files tok of [] => let - val keywords = Thy_Header.get_keywords thy; val master_dir = master_directory thy; val pos = Token.pos_of tok; - val src_paths = Keyword.command_files keywords cmd (Path.explode name); + val src_paths = make_paths (Path.explode name); in map (Command.read_file master_dir pos) src_paths end | files => map Exn.release files)); +val parse_file = parse_files single >> (fn f => f #> the_single); + + fun provide (src_path, id) = map_files (fn (master_dir, imports, provided) => if AList.defined (op =) provided src_path then error ("Duplicate use of source file: " ^ Path.print src_path) else (master_dir, imports, (src_path, id) :: provided)); fun provide_file (file: Token.file) = provide (#src_path file, #digest file); -fun provide_parse_files cmd = - parse_files cmd >> (fn files => fn thy => +fun provide_parse_files make_paths = + parse_files make_paths >> (fn files => fn thy => let val fs = files thy; val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; in (fs, thy') end); +val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); + + fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; in ((full_path, id), text) end; fun loaded_files_current thy = #provided (Files.get thy) |> forall (fn (src_path, id) => (case try (load_file thy) src_path of NONE => false | SOME ((_, id'), _) => id = id')); (* formal check *) fun formal_check check_file ctxt opt_dir (name, pos) = let fun err msg = error (msg ^ Position.here pos); val _ = Context_Position.report ctxt pos Markup.language_path; val dir = (case opt_dir of SOME dir => dir | NONE => master_directory (Proof_Context.theory_of ctxt)); val path = dir + Path.explode name handle ERROR msg => err msg; val _ = Path.expand path handle ERROR msg => err msg; val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); val _ = check_file path handle ERROR msg => err msg; in path end; val check_path = formal_check I; val check_file = formal_check File.check_file; val check_dir = formal_check File.check_dir; (* antiquotations *) local fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => let val _ = check ctxt NONE (name, pos); val latex = Latex.string (Latex.output_ascii_breakable "/" name); in Latex.enclose_block "\\isatt{" "}" [latex] end); fun ML_antiq check = Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path); in val _ = Theory.setup (Thy_Output.antiquotation_verbatim_embedded \<^binding>\session\ (Scan.lift Parse.embedded_position) check_session #> Thy_Output.antiquotation_verbatim_embedded \<^binding>\doc\ (Scan.lift Parse.embedded_position) check_doc #> Thy_Output.antiquotation_raw_embedded \<^binding>\path\ (document_antiq check_path) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\file\ (document_antiq check_file) (K I) #> Thy_Output.antiquotation_raw_embedded \<^binding>\dir\ (document_antiq check_dir) (K I) #> ML_Antiquotation.value_embedded \<^binding>\path\ (ML_antiq check_path) #> ML_Antiquotation.value_embedded \<^binding>\file\ (ML_antiq check_file) #> ML_Antiquotation.value_embedded \<^binding>\dir\ (ML_antiq check_dir) #> ML_Antiquotation.value_embedded \<^binding>\path_binding\ (Scan.lift (Parse.position Parse.path) >> (ML_Syntax.print_path_binding o Path.explode_binding)) #> ML_Antiquotation.value \<^binding>\master_dir\ (Args.theory >> (ML_Syntax.print_path o master_directory))); end; end; diff --git a/src/Pure/Pure.thy b/src/Pure/Pure.thy --- a/src/Pure/Pure.thy +++ b/src/Pure/Pure.thy @@ -1,1510 +1,1510 @@ (* Title: Pure/Pure.thy Author: Makarius The Pure theory, with definitions of Isar commands and some lemmas. *) theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" "obtains" "shows" "when" "where" "|" :: quasi_command and "text" "txt" :: document_body and "text_raw" :: document_raw and "default_sort" :: thy_decl and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations" "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias" "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn and "axiomatization" :: thy_stmt and "external_file" "bibtex_file" :: thy_load and "generate_file" :: thy_decl and "export_generated_files" :: diag and "compile_generated_files" :: diag and "external_files" "export_files" "export_prefix" and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML" and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML" and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML" and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *) and "ML_val" "ML_command" :: diag % "ML" and "simproc_setup" :: thy_decl % "ML" and "setup" "local_setup" "attribute_setup" "method_setup" "declaration" "syntax_declaration" "parse_ast_translation" "parse_translation" "print_translation" "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML" and "bundle" :: thy_decl_block and "unbundle" :: thy_decl and "include" "including" :: prf_decl and "print_bundles" :: diag and "context" "locale" "experiment" :: thy_decl_block and "interpret" :: prf_goal % "proof" and "interpretation" "global_interpretation" "sublocale" :: thy_goal and "class" :: thy_decl_block and "subclass" :: thy_goal and "instantiation" :: thy_decl_block and "instance" :: thy_goal and "overloading" :: thy_decl_block and "code_datatype" :: thy_decl and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt and "schematic_goal" :: thy_goal_stmt and "notepad" :: thy_decl_block and "have" :: prf_goal % "proof" and "hence" :: prf_goal % "proof" and "show" :: prf_asm_goal % "proof" and "thus" :: prf_asm_goal % "proof" and "then" "from" "with" :: prf_chain % "proof" and "note" :: prf_decl % "proof" and "supply" :: prf_script % "proof" and "using" "unfolding" :: prf_decl % "proof" and "fix" "assume" "presume" "define" :: prf_asm % "proof" and "consider" :: prf_goal % "proof" and "obtain" :: prf_asm_goal % "proof" and "guess" :: prf_script_asm_goal % "proof" and "let" "write" :: prf_decl % "proof" and "case" :: prf_asm % "proof" and "{" :: prf_open % "proof" and "}" :: prf_close % "proof" and "next" :: next_block % "proof" and "qed" :: qed_block % "proof" and "by" ".." "." "sorry" "\" :: "qed" % "proof" and "done" :: "qed_script" % "proof" and "oops" :: qed_global % "proof" and "defer" "prefer" "apply" :: prf_script % "proof" and "apply_end" :: prf_script % "proof" and "subgoal" :: prf_script_goal % "proof" and "proof" :: prf_block % "proof" and "also" "moreover" :: prf_decl % "proof" and "finally" "ultimately" :: prf_chain % "proof" and "back" :: prf_script % "proof" and "help" "print_commands" "print_options" "print_context" "print_theory" "print_definitions" "print_syntax" "print_abbrevs" "print_defn_rules" "print_theorems" "print_locales" "print_classes" "print_locale" "print_interps" "print_attributes" "print_simpset" "print_rules" "print_trans_rules" "print_methods" "print_antiquotations" "print_ML_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps" "thm_oracles" "print_term_bindings" "print_facts" "print_cases" "print_statement" "thm" "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms" :: diag and "print_state" :: diag and "welcome" :: diag and "end" :: thy_end and "realizers" :: thy_decl and "realizability" :: thy_decl and "extract_type" "extract" :: thy_decl and "find_theorems" "find_consts" :: diag and "named_theorems" :: thy_decl abbrevs "\\tag" = "\<^marker>\tag \" and "===>" = "===>" (*prevent replacement of very long arrows*) and "--->" = "\\" and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = "" and "hence" = "then have" and "thus" = "then show" begin section \Isar commands\ subsection \Other files\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\external_file\ "formal dependency on external file" - (Resources.provide_parse_files "external_file" >> (fn files => Toplevel.theory (#2 o files))); + (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (#2 o get_file))); val _ = Outer_Syntax.command \<^command_keyword>\bibtex_file\ "check bibtex database file in Prover IDE" - (Resources.provide_parse_files "bibtex_file" >> (fn files => + (Resources.provide_parse_file >> (fn get_file => Toplevel.theory (fn thy => let - val ([{lines, pos, ...}], thy') = files thy; + val ({lines, pos, ...}, thy') = get_file thy; val _ = Bibtex.check_database_output pos (cat_lines lines); in thy' end))); val _ = Outer_Syntax.local_theory \<^command_keyword>\generate_file\ "generate source file, with antiquotations" (Parse.path_binding -- (\<^keyword>\=\ |-- Parse.embedded_input) >> Generated_Files.generate_file_cmd); val files_in_theory = (Parse.underscore >> K [] || Scan.repeat1 Parse.path_binding) -- Scan.option (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.theory_name --| \<^keyword>\)\)); val _ = Outer_Syntax.command \<^command_keyword>\export_generated_files\ "export generated files from given theories" (Parse.and_list1 files_in_theory >> (fn args => Toplevel.keep (fn st => Generated_Files.export_generated_files_cmd (Toplevel.context_of st) args))); val base_dir = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (\<^keyword>\in\ |-- Parse.position Parse.path --| \<^keyword>\)\)) ("", Position.none); val external_files = Scan.repeat1 (Parse.position Parse.path) -- base_dir; val exe = Parse.reserved "exe" >> K true || Parse.reserved "executable" >> K false; val executable = \<^keyword>\(\ |-- Parse.!!! (exe --| \<^keyword>\)\) >> SOME || Scan.succeed NONE; val export_files = Scan.repeat1 Parse.path_binding -- executable; val _ = Outer_Syntax.command \<^command_keyword>\compile_generated_files\ "compile generated files and export results" (Parse.and_list files_in_theory -- Scan.optional (\<^keyword>\external_files\ |-- Parse.!!! (Parse.and_list1 external_files)) [] -- Scan.optional (\<^keyword>\export_files\ |-- Parse.!!! (Parse.and_list1 export_files)) [] -- Scan.optional (\<^keyword>\export_prefix\ |-- Parse.path_binding) ("", Position.none) -- (Parse.where_ |-- Parse.!!! Parse.ML_source) >> (fn ((((args, external), export), export_prefix), source) => Toplevel.keep (fn st => Generated_Files.compile_generated_files_cmd (Toplevel.context_of st) args external export export_prefix source))); in end\ subsection \Embedded ML text\ ML \ local val semi = Scan.option \<^keyword>\;\; val _ = Outer_Syntax.command \<^command_keyword>\ML_file\ "read and evaluate Isabelle/ML file" - (Resources.parse_files "ML_file" --| semi >> ML_File.ML NONE); + (Resources.parse_file --| semi >> ML_File.ML NONE); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_debug\ "read and evaluate Isabelle/ML file (with debugger information)" - (Resources.parse_files "ML_file_debug" --| semi >> ML_File.ML (SOME true)); + (Resources.parse_file --| semi >> ML_File.ML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\ML_file_no_debug\ "read and evaluate Isabelle/ML file (no debugger information)" - (Resources.parse_files "ML_file_no_debug" --| semi >> ML_File.ML (SOME false)); + (Resources.parse_file --| semi >> ML_File.ML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file\ "read and evaluate Standard ML file" - (Resources.parse_files "SML_file" --| semi >> ML_File.SML NONE); + (Resources.parse_file --| semi >> ML_File.SML NONE); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_debug\ "read and evaluate Standard ML file (with debugger information)" - (Resources.parse_files "SML_file_debug" --| semi >> ML_File.SML (SOME true)); + (Resources.parse_file --| semi >> ML_File.SML (SOME true)); val _ = Outer_Syntax.command \<^command_keyword>\SML_file_no_debug\ "read and evaluate Standard ML file (no debugger information)" - (Resources.parse_files "SML_file_no_debug" --| semi >> ML_File.SML (SOME false)); + (Resources.parse_file --| semi >> ML_File.SML (SOME false)); val _ = Outer_Syntax.command \<^command_keyword>\SML_export\ "evaluate SML within Isabelle/ML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_export, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.theory (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source))) end)); val _ = Outer_Syntax.command \<^command_keyword>\SML_import\ "evaluate Isabelle/ML within SML environment" (Parse.ML_source >> (fn source => let val flags: ML_Compiler.flags = {environment = ML_Env.SML_import, redirect = false, verbose = true, debug = NONE, writeln = writeln, warning = warning}; in Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source flags source) #> Local_Theory.propagate_ml_env) end)); val _ = Outer_Syntax.command ("ML_export", \<^here>) "ML text within theory or local theory, and export to bootstrap environment" (Parse.ML_source >> (fn source => Toplevel.generic_theory (fn context => context |> Config.put_generic ML_Env.ML_environment ML_Env.Isabelle |> Config.put_generic ML_Env.ML_write_global true |> ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) |> Config.restore_generic ML_Env.ML_write_global context |> Config.restore_generic ML_Env.ML_environment context |> Local_Theory.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source))) #> Proof.propagate_ml_env))); val _ = Outer_Syntax.command \<^command_keyword>\ML_val\ "diagnostic ML text" (Parse.ML_source >> Isar_Cmd.ml_diag true); val _ = Outer_Syntax.command \<^command_keyword>\ML_command\ "diagnostic ML text (silent)" (Parse.ML_source >> Isar_Cmd.ml_diag false); val _ = Outer_Syntax.command \<^command_keyword>\setup\ "ML setup for global theory" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.setup)); val _ = Outer_Syntax.local_theory \<^command_keyword>\local_setup\ "ML setup for local theory" (Parse.ML_source >> Isar_Cmd.local_setup); val _ = Outer_Syntax.command \<^command_keyword>\oracle\ "declare oracle" (Parse.range Parse.name -- (\<^keyword>\=\ |-- Parse.ML_source) >> (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y))); val _ = Outer_Syntax.local_theory \<^command_keyword>\attribute_setup\ "define attribute in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Attrib.attribute_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\method_setup\ "define proof method in ML" (Parse.name_position -- Parse.!!! (\<^keyword>\=\ |-- Parse.ML_source -- Scan.optional Parse.text "") >> (fn (name, (txt, cmt)) => Method.method_setup name txt cmt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\declaration\ "generic ML declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\syntax_declaration\ "generic ML syntax declaration" (Parse.opt_keyword "pervasive" -- Parse.ML_source >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt)); val _ = Outer_Syntax.local_theory \<^command_keyword>\simproc_setup\ "define simproc in ML" (Parse.name_position -- (\<^keyword>\(\ |-- Parse.enum1 "|" Parse.term --| \<^keyword>\)\ --| \<^keyword>\=\) -- Parse.ML_source >> (fn ((a, b), c) => Isar_Cmd.simproc_setup a b c)); in end\ subsection \Theory commands\ subsubsection \Sorts and types\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\default_sort\ "declare default sort for explicit type variables" (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy)); val _ = Outer_Syntax.local_theory \<^command_keyword>\typedecl\ "type declaration" (Parse.type_args -- Parse.binding -- Parse.opt_mixfix >> (fn ((args, a), mx) => Typedecl.typedecl {final = true} (a, map (rpair dummyS) args, mx) #> snd)); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_synonym\ "declare type abbreviation" (Parse.type_args -- Parse.binding -- (\<^keyword>\=\ |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')) >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)); in end\ subsubsection \Consts\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\judgment\ "declare object-logic judgment" (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\consts\ "declare constants" (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts_cmd)); in end\ subsubsection \Syntax and translations\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\nonterminal\ "declare syntactic type constructors (grammar nonterminal symbols)" (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global)); val _ = Outer_Syntax.command \<^command_keyword>\syntax\ "add raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\no_syntax\ "delete raw syntax clauses" (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); val trans_pat = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Parse.inner_syntax Parse.name --| \<^keyword>\)\)) "logic" -- Parse.inner_syntax Parse.string; fun trans_arrow toks = ((\<^keyword>\\\ || \<^keyword>\=>\) >> K Syntax.Parse_Rule || (\<^keyword>\\\ || \<^keyword>\<=\) >> K Syntax.Print_Rule || (\<^keyword>\\\ || \<^keyword>\==\) >> K Syntax.Parse_Print_Rule) toks; val trans_line = trans_pat -- Parse.!!! (trans_arrow -- trans_pat) >> (fn (left, (arr, right)) => arr (left, right)); val _ = Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); val _ = Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); in end\ subsubsection \Translation functions\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\parse_ast_translation\ "install parse ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation)); val _ = Outer_Syntax.command \<^command_keyword>\parse_translation\ "install parse translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_translation\ "install print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\typed_print_translation\ "install typed print translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation)); val _ = Outer_Syntax.command \<^command_keyword>\print_ast_translation\ "install print ast translation functions" (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation)); in end\ subsubsection \Specifications\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\definition\ "constant definition" (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) => #2 oo Specification.definition_cmd decl params prems spec)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\abbreviation\ "constant abbreviation" (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec)); val axiomatization = Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) -- Parse_Spec.if_assumes -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a)); val _ = Outer_Syntax.command \<^command_keyword>\axiomatization\ "axiomatic constant specification" (Scan.optional Parse.vars [] -- Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], []) >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d))); val _ = Outer_Syntax.local_theory \<^command_keyword>\alias\ "name-space alias for constant" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.alias_cmd); val _ = Outer_Syntax.local_theory \<^command_keyword>\type_alias\ "name-space alias for type constructor" (Parse.binding -- (Parse.!!! \<^keyword>\=\ |-- Parse.name_position) >> Specification.type_alias_cmd); in end\ subsubsection \Notation\ ML \ local val _ = Outer_Syntax.local_theory \<^command_keyword>\type_notation\ "add concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_type_notation\ "delete concrete syntax for type constructors" (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix) >> (fn (mode, args) => Specification.type_notation_cmd false mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\notation\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = Outer_Syntax.local_theory \<^command_keyword>\no_notation\ "delete concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Specification.notation_cmd false mode args)); in end\ subsubsection \Theorems\ ML \ local val long_keyword = Parse_Spec.includes >> K "" || Parse_Spec.long_statement_keyword; val long_statement = Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl)); val short_statement = Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (false, Binding.empty_atts, [], [Element.Fixes fixes, Element.Assumes assumes], Element.Shows shows)); fun theorem spec schematic descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) ((long_statement || short_statement) >> (fn (long, binding, includes, elems, concl) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) long Thm.theoremK NONE (K I) binding includes elems concl))); val _ = theorem \<^command_keyword>\theorem\ false "theorem"; val _ = theorem \<^command_keyword>\lemma\ false "lemma"; val _ = theorem \<^command_keyword>\corollary\ false "corollary"; val _ = theorem \<^command_keyword>\proposition\ false "proposition"; val _ = theorem \<^command_keyword>\schematic_goal\ true "schematic goal"; in end\ ML \ local val _ = Outer_Syntax.local_theory' \<^command_keyword>\lemmas\ "define theorems" (Parse_Spec.name_facts -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes)); val _ = Outer_Syntax.local_theory' \<^command_keyword>\declare\ "declare theorems" (Parse.and_list1 Parse.thms1 -- Parse.for_fixes >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd "" [(Binding.empty_atts, flat facts)] fixes)); val _ = Outer_Syntax.local_theory \<^command_keyword>\named_theorems\ "declare named collection of theorems" (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >> fold (fn (b, descr) => snd o Named_Theorems.declare b descr)); in end\ subsubsection \Hide names\ ML \ local fun hide_names command_keyword what hide parse prep = Outer_Syntax.command command_keyword ("hide " ^ what ^ " from name space") ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 parse >> (fn (fully, args) => (Toplevel.theory (fn thy => let val ctxt = Proof_Context.init_global thy in fold (hide fully o prep ctxt) args thy end)))); val _ = hide_names \<^command_keyword>\hide_class\ "classes" Sign.hide_class Parse.class Proof_Context.read_class; val _ = hide_names \<^command_keyword>\hide_type\ "types" Sign.hide_type Parse.type_const ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_const\ "consts" Sign.hide_const Parse.const ((#1 o dest_Const) oo Proof_Context.read_const {proper = true, strict = false}); val _ = hide_names \<^command_keyword>\hide_fact\ "facts" Global_Theory.hide_fact Parse.name_position (Global_Theory.check_fact o Proof_Context.theory_of); in end\ subsection \Bundled declarations\ ML \ local val _ = Outer_Syntax.maybe_begin_local_theory \<^command_keyword>\bundle\ "define bundle of declarations" ((Parse.binding --| \<^keyword>\=\) -- Parse.thms1 -- Parse.for_fixes >> (uncurry Bundle.bundle_cmd)) (Parse.binding --| Parse.begin >> Bundle.init); val _ = Outer_Syntax.local_theory \<^command_keyword>\unbundle\ "activate declarations from bundle in local theory" (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd); val _ = Outer_Syntax.command \<^command_keyword>\include\ "activate declarations from bundle in proof body" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\including\ "activate declarations from bundle in goal refinement" (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\print_bundles\ "print bundles of declarations" (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of))); in end\ subsection \Local theory specifications\ subsubsection \Specification context\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\context\ "begin local theory context" ((Parse.name_position >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd [] name)) || Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems))) --| Parse.begin); val _ = Outer_Syntax.command \<^command_keyword>\end\ "end context" (Scan.succeed (Toplevel.exit o Toplevel.end_main_target o Toplevel.end_nested_target o Toplevel.end_proof (K Proof.end_notepad))); in end\ subsubsection \Locales and interpretation\ ML \ local val locale_context_elements = Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element; val locale_val = Parse_Spec.locale_expression -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! locale_context_elements) ([], []) || locale_context_elements >> pair ([], []); val _ = Outer_Syntax.command \<^command_keyword>\locale\ "define named specification context" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- Parse.!!! locale_val) (([], []), ([], [])) -- Parse.opt_begin >> (fn ((name, (expr, (includes, elems))), begin) => Toplevel.begin_main_target begin (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\experiment\ "open private specification context" (Scan.repeat Parse_Spec.context_element --| Parse.begin >> (fn elems => Toplevel.begin_main_target true (Experiment.experiment_cmd elems #> snd))); val _ = Outer_Syntax.command \<^command_keyword>\interpret\ "prove interpretation of locale expression in proof context" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.proof (Interpretation.interpret_cmd expr))); val interpretation_args_with_defs = Parse.!!! Parse_Spec.locale_expression -- (Scan.optional (\<^keyword>\defines\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term))) ([])); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\global_interpretation\ "prove interpretation of locale expression into global theory" (interpretation_args_with_defs >> (fn (expr, defs) => Interpretation.global_interpretation_cmd expr defs)); val _ = Outer_Syntax.command \<^command_keyword>\sublocale\ "prove sublocale relation between a locale and a locale expression" ((Parse.name_position --| (\<^keyword>\\\ || \<^keyword>\<\) -- interpretation_args_with_defs >> (fn (loc, (expr, defs)) => Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs))) || interpretation_args_with_defs >> (fn (expr, defs) => Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs))); val _ = Outer_Syntax.command \<^command_keyword>\interpretation\ "prove interpretation of locale expression in local theory or into global theory" (Parse.!!! Parse_Spec.locale_expression >> (fn expr => Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr))); in end\ subsubsection \Type classes\ ML \ local val class_context_elements = Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element; val class_val = Parse_Spec.class_expression -- Scan.optional (\<^keyword>\+\ |-- Parse.!!! class_context_elements) ([], []) || class_context_elements >> pair []; val _ = Outer_Syntax.command \<^command_keyword>\class\ "define type class" (Parse.binding -- Scan.optional (\<^keyword>\=\ |-- class_val) ([], ([], [])) -- Parse.opt_begin >> (fn ((name, (supclasses, (includes, elems))), begin) => Toplevel.begin_main_target begin (Class_Declaration.class_cmd name includes supclasses elems #> snd))); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\subclass\ "prove a subclass relation" (Parse.class >> Class_Declaration.subclass_cmd); val _ = Outer_Syntax.command \<^command_keyword>\instantiation\ "instantiate and prove type arity" (Parse.multi_arity --| Parse.begin >> (fn arities => Toplevel.begin_main_target true (Class.instantiation_cmd arities))); val _ = Outer_Syntax.command \<^command_keyword>\instance\ "prove type arity or subclass relation" ((Parse.class -- ((\<^keyword>\\\ || \<^keyword>\<\) |-- Parse.!!! Parse.class) >> Class.classrel_cmd || Parse.multi_arity >> Class.instance_arity_cmd) >> Toplevel.theory_to_proof || Scan.succeed (Toplevel.local_theory_to_proof NONE NONE (Class.instantiation_instance I))); in end\ subsubsection \Arbitrary overloading\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\overloading\ "overloaded definitions" (Scan.repeat1 (Parse.name --| (\<^keyword>\==\ || \<^keyword>\\\) -- Parse.term -- Scan.optional (\<^keyword>\(\ |-- (\<^keyword>\unchecked\ >> K false) --| \<^keyword>\)\) true >> Scan.triple1) --| Parse.begin >> (fn operations => Toplevel.begin_main_target true (Overloading.overloading_cmd operations))); in end\ subsection \Proof commands\ ML \ local val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\notepad\ "begin proof context" (Parse.begin >> K Proof.begin_notepad); in end\ subsubsection \Statements\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.cond_statement -- Parse.for_fixes >> (fn ((shows, (strict, assumes)), fixes) => (strict, fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\have\ "state local goal" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\show\ "state local goal, to refine pending subgoals" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.show_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\hence\ "old-style alias of \"then have\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd a NONE (K I) b c d int #> #2))); val _ = Outer_Syntax.command \<^command_keyword>\thus\ "old-style alias of \"then show\"" (structured_statement >> (fn (a, b, c, d) => Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd a NONE (K I) b c d int #> #2))); in end\ subsubsection \Local facts\ ML \ local val facts = Parse.and_list1 Parse.thms1; val _ = Outer_Syntax.command \<^command_keyword>\then\ "forward chaining" (Scan.succeed (Toplevel.proof Proof.chain)); val _ = Outer_Syntax.command \<^command_keyword>\from\ "forward chaining from given facts" (facts >> (Toplevel.proof o Proof.from_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\with\ "forward chaining from given and current facts" (facts >> (Toplevel.proof o Proof.with_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\note\ "define facts" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.note_thmss_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\supply\ "define facts during goal refinement (unstructured)" (Parse_Spec.name_facts >> (Toplevel.proof o Proof.supply_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\using\ "augment goal facts" (facts >> (Toplevel.proof o Proof.using_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\unfolding\ "unfold definitions in goal and facts" (facts >> (Toplevel.proof o Proof.unfolding_cmd)); in end\ subsubsection \Proof context\ ML \ local val structured_statement = Parse_Spec.statement -- Parse_Spec.if_statement' -- Parse.for_fixes >> (fn ((shows, assumes), fixes) => (fixes, assumes, shows)); val _ = Outer_Syntax.command \<^command_keyword>\fix\ "fix local variables (Skolem constants)" (Parse.vars >> (Toplevel.proof o Proof.fix_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\assume\ "assume propositions" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.assume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\presume\ "assume propositions, to be established later" (structured_statement >> (fn (a, b, c) => Toplevel.proof (Proof.presume_cmd a b c))); val _ = Outer_Syntax.command \<^command_keyword>\define\ "local definition (non-polymorphic)" ((Parse.vars --| Parse.where_) -- Parse_Spec.statement -- Parse.for_fixes >> (fn ((a, b), c) => Toplevel.proof (Proof.define_cmd a c b))); val _ = Outer_Syntax.command \<^command_keyword>\consider\ "state cases rule" (Parse_Spec.obtains >> (Toplevel.proof' o Obtain.consider_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\obtain\ "generalized elimination" (Parse.parbinding -- Scan.optional (Parse.vars --| Parse.where_) [] -- structured_statement >> (fn ((a, b), (c, d, e)) => Toplevel.proof' (Obtain.obtain_cmd a b c d e))); val _ = Outer_Syntax.command \<^command_keyword>\guess\ "wild guessing (unstructured)" (Scan.optional Parse.vars [] >> (Toplevel.proof' o Obtain.guess_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\let\ "bind text variables" (Parse.and_list1 (Parse.and_list1 Parse.term -- (\<^keyword>\=\ |-- Parse.term)) >> (Toplevel.proof o Proof.let_bind_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\write\ "add concrete syntax for constants / fixed variables" (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix) >> (fn (mode, args) => Toplevel.proof (Proof.write_cmd mode args))); val _ = Outer_Syntax.command \<^command_keyword>\case\ "invoke local context" (Parse_Spec.opt_thm_name ":" -- (\<^keyword>\(\ |-- Parse.!!! (Parse.name_position -- Scan.repeat (Parse.maybe Parse.binding) --| \<^keyword>\)\) || Parse.name_position >> rpair []) >> (Toplevel.proof o Proof.case_cmd)); in end\ subsubsection \Proof structure\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\{\ "begin explicit proof block" (Scan.succeed (Toplevel.proof Proof.begin_block)); val _ = Outer_Syntax.command \<^command_keyword>\}\ "end explicit proof block" (Scan.succeed (Toplevel.proof Proof.end_block)); val _ = Outer_Syntax.command \<^command_keyword>\next\ "enter next proof block" (Scan.succeed (Toplevel.proof Proof.next_block)); in end\ subsubsection \End proof\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\qed\ "conclude proof" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m))); val _ = Outer_Syntax.command \<^command_keyword>\by\ "terminal backward proof" (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) => (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2)))); val _ = Outer_Syntax.command \<^command_keyword>\..\ "default proof" (Scan.succeed Isar_Cmd.default_proof); val _ = Outer_Syntax.command \<^command_keyword>\.\ "immediate proof" (Scan.succeed Isar_Cmd.immediate_proof); val _ = Outer_Syntax.command \<^command_keyword>\done\ "done proof" (Scan.succeed Isar_Cmd.done_proof); val _ = Outer_Syntax.command \<^command_keyword>\sorry\ "skip proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\\\ "dummy proof (quick-and-dirty mode only!)" (Scan.succeed Isar_Cmd.skip_proof); val _ = Outer_Syntax.command \<^command_keyword>\oops\ "forget proof" (Scan.succeed Toplevel.forget_proof); in end\ subsubsection \Proof steps\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\defer\ "shuffle internal proof state" (Scan.optional Parse.nat 1 >> (Toplevel.proof o Proof.defer)); val _ = Outer_Syntax.command \<^command_keyword>\prefer\ "shuffle internal proof state" (Parse.nat >> (Toplevel.proof o Proof.prefer)); val _ = Outer_Syntax.command \<^command_keyword>\apply\ "initial goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m)))); val _ = Outer_Syntax.command \<^command_keyword>\apply_end\ "terminal goal refinement step (unstructured)" (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m)))); val _ = Outer_Syntax.command \<^command_keyword>\proof\ "backward proof step" (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Toplevel.proof (fn state => let val state' = state |> Proof.proof m |> Seq.the_result ""; val _ = Output.information (Proof_Context.print_cases_proof (Proof.context_of state) (Proof.context_of state')); in state' end)))) in end\ subsubsection \Subgoal focus\ ML \ local val opt_fact_binding = Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) Binding.empty_atts; val for_params = Scan.optional (\<^keyword>\for\ |-- Parse.!!! ((Scan.option Parse.dots >> is_some) -- (Scan.repeat1 (Parse.maybe_position Parse.name_position)))) (false, []); val _ = Outer_Syntax.command \<^command_keyword>\subgoal\ "focus on first subgoal within backward refinement" (opt_fact_binding -- (Scan.option (\<^keyword>\premises\ |-- Parse.!!! opt_fact_binding)) -- for_params >> (fn ((a, b), c) => Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c))); in end\ subsubsection \Calculation\ ML \ local val calculation_args = Scan.option (\<^keyword>\(\ |-- Parse.!!! ((Parse.thms1 --| \<^keyword>\)\))); val _ = Outer_Syntax.command \<^command_keyword>\also\ "combine calculation and current facts" (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\finally\ "combine calculation and current facts, exhibit result" (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd)); val _ = Outer_Syntax.command \<^command_keyword>\moreover\ "augment calculation by current facts" (Scan.succeed (Toplevel.proof' Calculation.moreover)); val _ = Outer_Syntax.command \<^command_keyword>\ultimately\ "augment calculation by current facts, exhibit result" (Scan.succeed (Toplevel.proof' Calculation.ultimately)); val _ = Outer_Syntax.command \<^command_keyword>\print_trans_rules\ "print transitivity rules" (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of))); in end\ subsubsection \Proof navigation\ ML \ local fun report_back () = Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"]; val _ = Outer_Syntax.command \<^command_keyword>\back\ "explicit backtracking of proof command" (Scan.succeed (Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o Toplevel.skip_proof report_back)); in end\ subsection \Diagnostic commands (for interactive mode only)\ ML \ local val opt_modes = Scan.optional (\<^keyword>\(\ |-- Parse.!!! (Scan.repeat1 Parse.name --| \<^keyword>\)\)) []; val _ = Outer_Syntax.command \<^command_keyword>\help\ "retrieve outer syntax commands according to name patterns" (Scan.repeat Parse.name >> (fn pats => Toplevel.keep (fn st => Outer_Syntax.help (Toplevel.theory_of st) pats))); val _ = Outer_Syntax.command \<^command_keyword>\print_commands\ "print outer syntax commands" (Scan.succeed (Toplevel.keep (Outer_Syntax.print_commands o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_options\ "print configuration options" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_context\ "print context of local theory target" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context))); val _ = Outer_Syntax.command \<^command_keyword>\print_theory\ "print logical theory contents" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_theory b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_definitions\ "print dependencies of definitional theory content" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Proof_Display.pretty_definitions b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_syntax\ "print inner syntax of context" (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_defn_rules\ "print definitional rewrite rules of context" (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_abbrevs\ "print constant abbreviations of context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_theorems\ "print theorems of local theory or proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b))); val _ = Outer_Syntax.command \<^command_keyword>\print_locales\ "print locales of this theory" (Parse.opt_bang >> (fn verbose => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in Pretty.writeln (Locale.pretty_locales thy verbose) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_classes\ "print classes of this theory" (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_locale\ "print locale of this theory" (Parse.opt_bang -- Parse.name_position >> (fn (show_facts, raw_name) => Toplevel.keep (fn state => let val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_locale thy show_facts name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_interps\ "print interpretations of locale for this theory or proof context" (Parse.name_position >> (fn raw_name => Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state; val thy = Toplevel.theory_of state; val name = Locale.check thy raw_name; in Pretty.writeln (Locale.pretty_registrations ctxt name) end))); val _ = Outer_Syntax.command \<^command_keyword>\print_attributes\ "print attributes of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_simpset\ "print context of Simplifier" (Parse.opt_bang >> (fn b => Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_rules\ "print intro/elim rules" (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_methods\ "print methods of this theory" (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_antiquotations\ "print document antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (Document_Antiquotation.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_ML_antiquotations\ "print ML antiquotations" (Parse.opt_bang >> (fn b => Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\locale_deps\ "visualize locale dependencies" (Scan.succeed (Toplevel.keep (Toplevel.theory_of #> (fn thy => Locale.pretty_locale_deps thy |> map (fn {name, parents, body} => ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents)) |> Graph_Display.display_graph_old)))); val _ = Outer_Syntax.command \<^command_keyword>\print_term_bindings\ "print term bindings of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_facts\ "print facts of proof context" (Parse.opt_bang >> (fn b => Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_cases\ "print cases of proof context" (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_statement\ "print theorems as long statements" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_stmts); val _ = Outer_Syntax.command \<^command_keyword>\thm\ "print theorems" (opt_modes -- Parse.thms1 >> Isar_Cmd.print_thms); val _ = Outer_Syntax.command \<^command_keyword>\prf\ "print proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs false); val _ = Outer_Syntax.command \<^command_keyword>\full_prf\ "print full proof terms of theorems" (opt_modes -- Scan.option Parse.thms1 >> Isar_Cmd.print_prfs true); val _ = Outer_Syntax.command \<^command_keyword>\prop\ "read and print proposition" (opt_modes -- Parse.term >> Isar_Cmd.print_prop); val _ = Outer_Syntax.command \<^command_keyword>\term\ "read and print term" (opt_modes -- Parse.term >> Isar_Cmd.print_term); val _ = Outer_Syntax.command \<^command_keyword>\typ\ "read and print type" (opt_modes -- (Parse.typ -- Scan.option (\<^keyword>\::\ |-- Parse.!!! Parse.sort)) >> Isar_Cmd.print_type); val _ = Outer_Syntax.command \<^command_keyword>\print_codesetup\ "print code generator setup" (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of))); val _ = Outer_Syntax.command \<^command_keyword>\print_state\ "print current proof state (if present)" (opt_modes >> (fn modes => Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state)))); val _ = Outer_Syntax.command \<^command_keyword>\welcome\ "print welcome message" (Scan.succeed (Toplevel.keep (fn _ => writeln (Session.welcome ())))); in end\ subsection \Dependencies\ ML \ local val theory_bounds = Parse.theory_name >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.theory_name --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\thy_deps\ "visualize theory dependencies" (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args))); val class_bounds = Parse.sort >> single || (\<^keyword>\(\ |-- Parse.enum "|" Parse.sort --| \<^keyword>\)\); val _ = Outer_Syntax.command \<^command_keyword>\class_deps\ "visualize class dependencies" (Scan.option class_bounds -- Scan.option class_bounds >> (fn args => Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args))); val _ = Outer_Syntax.command \<^command_keyword>\thm_deps\ "print theorem dependencies (immediate non-transitive)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ "print all oracles used in theorems (full graph of transitive dependencies)" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => let val ctxt = Toplevel.context_of st; val thms = Attrib.eval_thms ctxt args; in Pretty.writeln (Thm_Deps.pretty_thm_oracles ctxt thms) end))); val thy_names = Scan.repeat1 (Scan.unless Parse.minus Parse.theory_name); val _ = Outer_Syntax.command \<^command_keyword>\unused_thms\ "find unused theorems" (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range => Toplevel.keep (fn st => let val thy = Toplevel.theory_of st; val ctxt = Toplevel.context_of st; fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); val check = Theory.check {long = false} ctxt; in Thm_Deps.unused_thms_cmd (case opt_range of NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) | SOME (xs, SOME ys) => (map check xs, map check ys)) |> map pretty_thm |> Pretty.writeln_chunks end))); in end\ subsubsection \Find consts and theorems\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\find_consts\ "find constants by name / type patterns" (Find_Consts.query_parser >> (fn spec => Toplevel.keep (fn st => Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec)))); val options = Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")")) (NONE, true); val _ = Outer_Syntax.command \<^command_keyword>\find_theorems\ "find theorems meeting specified criteria" (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) => Toplevel.keep (fn st => Pretty.writeln (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec)))); in end\ subsection \Code generation\ ML \ local val _ = Outer_Syntax.command \<^command_keyword>\code_datatype\ "define set of code datatype constructors" (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.declare_datatype_cmd)); in end\ subsection \Extraction of programs from proofs\ ML \ local val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") []; val _ = Outer_Syntax.command \<^command_keyword>\realizers\ "specify realizers for primitive axioms / theorems, together with correctness proof" (Scan.repeat1 (Parse.name -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >> (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy))); val _ = Outer_Syntax.command \<^command_keyword>\realizability\ "add equations characterizing realizability" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract_type\ "add equations characterizing type of extracted program" (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns)); val _ = Outer_Syntax.command \<^command_keyword>\extract\ "extract terms from proofs" (Scan.repeat1 (Parse.name -- parse_vars) >> (fn xs => Toplevel.theory (fn thy => Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy))); in end\ section \Auxiliary lemmas\ subsection \Meta-level connectives in assumptions\ lemma meta_mp: assumes "PROP P \ PROP Q" and "PROP P" shows "PROP Q" by (rule \PROP P \ PROP Q\ [OF \PROP P\]) lemmas meta_impE = meta_mp [elim_format] lemma meta_spec: assumes "\x. PROP P x" shows "PROP P x" by (rule \\x. PROP P x\) lemmas meta_allE = meta_spec [elim_format] lemma swap_params: "(\x y. PROP P x y) \ (\y x. PROP P x y)" .. lemma equal_allI: \(\x. PROP P x) \ (\x. PROP Q x)\ if \\x. PROP P x \ PROP Q x\ by (simp only: that) subsection \Meta-level conjunction\ lemma all_conjunction: "(\x. PROP A x &&& PROP B x) \ ((\x. PROP A x) &&& (\x. PROP B x))" proof assume conj: "\x. PROP A x &&& PROP B x" show "(\x. PROP A x) &&& (\x. PROP B x)" proof - fix x from conj show "PROP A x" by (rule conjunctionD1) from conj show "PROP B x" by (rule conjunctionD2) qed next assume conj: "(\x. PROP A x) &&& (\x. PROP B x)" fix x show "PROP A x &&& PROP B x" proof - show "PROP A x" by (rule conj [THEN conjunctionD1, rule_format]) show "PROP B x" by (rule conj [THEN conjunctionD2, rule_format]) qed qed lemma imp_conjunction: "(PROP A \ PROP B &&& PROP C) \ ((PROP A \ PROP B) &&& (PROP A \ PROP C))" proof assume conj: "PROP A \ PROP B &&& PROP C" show "(PROP A \ PROP B) &&& (PROP A \ PROP C)" proof - assume "PROP A" from conj [OF \PROP A\] show "PROP B" by (rule conjunctionD1) from conj [OF \PROP A\] show "PROP C" by (rule conjunctionD2) qed next assume conj: "(PROP A \ PROP B) &&& (PROP A \ PROP C)" assume "PROP A" show "PROP B &&& PROP C" proof - from \PROP A\ show "PROP B" by (rule conj [THEN conjunctionD1]) from \PROP A\ show "PROP C" by (rule conj [THEN conjunctionD2]) qed qed lemma conjunction_imp: "(PROP A &&& PROP B \ PROP C) \ (PROP A \ PROP B \ PROP C)" proof assume r: "PROP A &&& PROP B \ PROP C" assume ab: "PROP A" "PROP B" show "PROP C" proof (rule r) from ab show "PROP A &&& PROP B" . qed next assume r: "PROP A \ PROP B \ PROP C" assume conj: "PROP A &&& PROP B" show "PROP C" proof (rule r) from conj show "PROP A" by (rule conjunctionD1) from conj show "PROP B" by (rule conjunctionD2) qed qed declare [[ML_write_global = false]] end diff --git a/src/Pure/Thy/thy_header.ML b/src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML +++ b/src/Pure/Thy/thy_header.ML @@ -1,212 +1,214 @@ (* Title: Pure/Thy/thy_header.ML Author: Makarius Static theory header information. *) signature THY_HEADER = sig type keywords = ((string * Position.T) * Keyword.spec) list type header = {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords} val make: string * Position.T -> (string * Position.T) list -> keywords -> header val theoryN: string val bootstrap_keywords: Keyword.keywords val add_keywords: keywords -> theory -> theory val get_keywords: theory -> Keyword.keywords val get_keywords': Proof.context -> Keyword.keywords val ml_bootstrapN: string val ml_roots: string list val bootstrap_thys: string list val is_base_name: string -> bool val import_name: string -> string val args: header parser val read_tokens: Position.T -> Token.T list -> header val read: Position.T -> string -> header end; structure Thy_Header: THY_HEADER = struct (** keyword declarations **) (* header *) type keywords = ((string * Position.T) * Keyword.spec) list; type header = {name: string * Position.T, imports: (string * Position.T) list, keywords: keywords}; fun make name imports keywords : header = {name = name, imports = imports, keywords = keywords}; (* bootstrap keywords *) val chapterN = "chapter"; val sectionN = "section"; val subsectionN = "subsection"; val subsubsectionN = "subsubsection"; val paragraphN = "paragraph"; val subparagraphN = "subparagraph"; val textN = "text"; val txtN = "txt"; val text_rawN = "text_raw"; val theoryN = "theory"; val importsN = "imports"; val keywordsN = "keywords"; val abbrevsN = "abbrevs"; val beginN = "begin"; val bootstrap_keywords = Keyword.empty_keywords |> Keyword.add_keywords [(("%", \<^here>), Keyword.no_spec), (("(", \<^here>), Keyword.no_spec), ((")", \<^here>), Keyword.no_spec), ((",", \<^here>), Keyword.no_spec), (("::", \<^here>), Keyword.no_spec), (("=", \<^here>), Keyword.no_spec), (("and", \<^here>), Keyword.no_spec), ((beginN, \<^here>), Keyword.quasi_command_spec), ((importsN, \<^here>), Keyword.quasi_command_spec), ((keywordsN, \<^here>), Keyword.quasi_command_spec), ((abbrevsN, \<^here>), Keyword.quasi_command_spec), ((chapterN, \<^here>), Keyword.document_heading_spec), ((sectionN, \<^here>), Keyword.document_heading_spec), ((subsectionN, \<^here>), Keyword.document_heading_spec), ((subsubsectionN, \<^here>), Keyword.document_heading_spec), ((paragraphN, \<^here>), Keyword.document_heading_spec), ((subparagraphN, \<^here>), Keyword.document_heading_spec), ((textN, \<^here>), Keyword.document_body_spec), ((txtN, \<^here>), Keyword.document_body_spec), - ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])), - ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])), - (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))]; + ((text_rawN, \<^here>), (Keyword.document_raw, ["document"])), + ((theoryN, \<^here>), (Keyword.thy_begin, ["theory"])), + (("ML", \<^here>), (Keyword.thy_decl, ["ML"]))]; (* theory data *) structure Data = Theory_Data ( type T = Keyword.keywords; val empty = bootstrap_keywords; val extend = I; val merge = Keyword.merge_keywords; ); val add_keywords = Data.map o Keyword.add_keywords; val get_keywords = Data.get; val get_keywords' = get_keywords o Proof_Context.theory_of; (** concrete syntax **) (* names *) val ml_bootstrapN = "ML_Bootstrap"; val ml_roots = ["ML_Root0", "ML_Root"]; val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"]; fun is_base_name s = s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) fun import_name s = if String.isSuffix ".thy" s then error ("Malformed theory import: " ^ quote s) else Path.file_name (Path.explode s); (* header args *) local fun imports name = if name = Context.PureN then Scan.succeed [] else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 Parse.theory_name); -val opt_files = - Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") []; +fun loaded_files kind = + if kind = Keyword.thy_load then + Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [] + else Scan.succeed []; val keyword_spec = Parse.group (fn () => "outer syntax keyword specification") - (Parse.name -- opt_files -- Document_Source.old_tags); + ((Parse.name :-- loaded_files >> #1) -- Document_Source.old_tags); val keyword_decl = Scan.repeat1 Parse.string_position -- Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec >> (fn (names, spec) => map (rpair spec) names); val abbrevs = Parse.and_list1 (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text)) >> uncurry (map_product pair)) >> flat; val keyword_decls = Parse.and_list1 keyword_decl >> flat; in val args = Parse.theory_name :|-- (fn (name, pos) => imports name -- Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --| (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN) >> (fn (imports, keywords) => make (name, pos) imports keywords)); end; (* read header *) val heading = (Parse.command_name chapterN || Parse.command_name sectionN || Parse.command_name subsectionN || Parse.command_name subsubsectionN || Parse.command_name paragraphN || Parse.command_name subparagraphN || Parse.command_name textN || Parse.command_name txtN || Parse.command_name text_rawN) -- (Document_Source.annotation |-- Parse.!!! Parse.document_source); val parse_header = (Scan.repeat heading -- Parse.command_name theoryN --| Document_Source.annotation) |-- Parse.!!! args; fun read_tokens pos toks = filter Token.is_proper toks |> Source.of_list |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! parse_header))) |> Source.get_single |> (fn SOME (header, _) => header | NONE => error ("Unexpected end of input" ^ Position.here pos)); local fun read_header pos text = Symbol_Pos.explode (text, pos) |> Token.tokenize bootstrap_keywords {strict = false} |> read_tokens pos; val approx_length = 1024; in fun read pos text = if size text <= approx_length then read_header pos text else let val approx_text = String.substring (text, 0, approx_length) in if String.isSuffix "begin" approx_text then read_header pos text else (read_header pos approx_text handle ERROR _ => read_header pos text) end; end; end; diff --git a/src/Pure/Thy/thy_header.scala b/src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala +++ b/src/Pure/Thy/thy_header.scala @@ -1,243 +1,243 @@ /* Title: Pure/Thy/thy_header.scala Author: Makarius Static theory header information. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.util.parsing.input.Reader import scala.util.matching.Regex object Thy_Header { /* bootstrap keywords */ type Keywords = List[(String, Keyword.Spec)] type Abbrevs = List[(String, String)] val CHAPTER = "chapter" val SECTION = "section" val SUBSECTION = "subsection" val SUBSUBSECTION = "subsubsection" val PARAGRAPH = "paragraph" val SUBPARAGRAPH = "subparagraph" val TEXT = "text" val TXT = "txt" val TEXT_RAW = "text_raw" val THEORY = "theory" val IMPORTS = "imports" val KEYWORDS = "keywords" val ABBREVS = "abbrevs" val AND = "and" val BEGIN = "begin" val bootstrap_header: Keywords = List( ("%", Keyword.Spec.none), ("(", Keyword.Spec.none), (")", Keyword.Spec.none), (",", Keyword.Spec.none), ("::", Keyword.Spec.none), ("=", Keyword.Spec.none), (AND, Keyword.Spec.none), (BEGIN, Keyword.Spec(Keyword.QUASI_COMMAND)), (IMPORTS, Keyword.Spec(Keyword.QUASI_COMMAND)), (KEYWORDS, Keyword.Spec(Keyword.QUASI_COMMAND)), (ABBREVS, Keyword.Spec(Keyword.QUASI_COMMAND)), (CHAPTER, Keyword.Spec(Keyword.DOCUMENT_HEADING)), (SECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)), (SUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)), (SUBSUBSECTION, Keyword.Spec(Keyword.DOCUMENT_HEADING)), (PARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)), (SUBPARAGRAPH, Keyword.Spec(Keyword.DOCUMENT_HEADING)), (TEXT, Keyword.Spec(Keyword.DOCUMENT_BODY)), (TXT, Keyword.Spec(Keyword.DOCUMENT_BODY)), (TEXT_RAW, Keyword.Spec(Keyword.DOCUMENT_RAW)), (THEORY, Keyword.Spec(Keyword.THY_BEGIN, tags = List("theory"))), ("ML", Keyword.Spec(Keyword.THY_DECL, tags = List("ML")))) private val bootstrap_keywords = Keyword.Keywords.empty.add_keywords(bootstrap_header) val bootstrap_syntax: Outer_Syntax = Outer_Syntax.empty.add_keywords(bootstrap_header) /* file name vs. theory name */ val PURE = "Pure" val ML_BOOTSTRAP = "ML_Bootstrap" val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root") val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a)) val bootstrap_global_theories = (Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE) private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""") private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""") private val File_Name = new Regex(""".*?([^/\\:]+)""") def is_base_name(s: String): Boolean = s != "" && !s.exists("/\\:".contains(_)) def split_file_name(s: String): Option[(String, String)] = s match { case Split_File_Name(s1, s2) => Some((s1, s2)) case _ => None } def import_name(s: String): String = s match { case File_Name(name) if !name.endsWith(".thy") => name case _ => error("Malformed theory import: " + quote(s)) } def theory_name(s: String): String = s match { case Thy_File_Name(name) => bootstrap_name(name) case File_Name(name) => if (name == Sessions.root_name) name else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("") case _ => "" } def is_ml_root(theory: String): Boolean = ml_roots.exists({ case (_, b) => b == theory }) def is_bootstrap(theory: String): Boolean = bootstrap_thys.exists({ case (_, b) => b == theory }) def bootstrap_name(theory: String): String = bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory) def try_read_dir(dir: Path): List[String] = { val files = try { File.read_dir(dir) } catch { case ERROR(_) => Nil } for { Thy_File_Name(name) <- files } yield name } /* parser */ trait Parser extends Parse.Parser { val header: Parser[Thy_Header] = { - val opt_files = + val loaded_files = $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } | success(Nil) val keyword_spec = - atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^ + atom("outer syntax keyword specification", _.is_name) ~ loaded_files ~ tags ^^ { case x ~ y ~ z => Keyword.Spec(x, y, z) } val keyword_decl = rep1(string) ~ opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^ { case xs ~ y => xs.map((_, y.getOrElse(Keyword.Spec.none))) } val keyword_decls = keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^ { case xs ~ yss => (xs :: yss).flatten } val abbrevs = rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^ { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) } val args = position(theory_name) ~ (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(ABBREVS) ~! abbrevs) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ $$$(BEGIN) ^^ { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ => val f = Symbol.decode _ Thy_Header((f(name), pos), imports.map({ case (a, b) => (f(a), b) }), keywords.map({ case (a, Keyword.Spec(b, c, d)) => (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }), abbrevs.map({ case (a, b) => (f(a), f(b)) })) } val heading = (command(CHAPTER) | command(SECTION) | command(SUBSECTION) | command(SUBSUBSECTION) | command(PARAGRAPH) | command(SUBPARAGRAPH) | command(TEXT) | command(TXT) | command(TEXT_RAW)) ~ annotation ~! document_source (rep(heading) ~ command(THEORY) ~ annotation) ~! args ^^ { case _ ~ x => x } } } /* read -- lazy scanning */ private def read_tokens(reader: Reader[Char], strict: Boolean): (List[Token], List[Token]) = { val token = Token.Parsers.token(bootstrap_keywords) def make_tokens(in: Reader[Char]): Stream[Token] = token(in) match { case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) case _ => Stream.empty } val all_tokens = make_tokens(reader) val drop_tokens = if (strict) Nil else all_tokens.takeWhile(tok => !tok.is_command(Thy_Header.THEORY)).toList val tokens = all_tokens.drop(drop_tokens.length) val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList (drop_tokens, tokens1 ::: tokens2) } private object Parser extends Parser { def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header = parse(commit(header), Token.reader(tokens, pos)) match { case Success(result, _) => result case bad => error(bad.toString) } } def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = { val (_, tokens0) = read_tokens(reader, true) val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0)) val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict) val pos = (start /: drop_tokens)(_.advance(_)) Parser.parse_header(tokens, pos) } } sealed case class Thy_Header( name_pos: (String, Position.T), imports_pos: List[(String, Position.T)], keywords: Thy_Header.Keywords, abbrevs: Thy_Header.Abbrevs) { def name: String = name_pos._1 def pos: Position.T = name_pos._2 def imports: List[String] = imports_pos.map(_._1) }