diff --git a/src/Pure/Isar/outer_syntax.ML b/src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML +++ b/src/Pure/Isar/outer_syntax.ML @@ -1,333 +1,332 @@ (* Title: Pure/Isar/outer_syntax.ML Author: Markus Wenzel, TU Muenchen Isabelle/Isar outer syntax. *) signature OUTER_SYNTAX = sig val help: theory -> string list -> unit val print_commands: theory -> unit type command_keyword = string * Position.T val command: command_keyword -> string -> (Toplevel.transition -> Toplevel.transition) parser -> unit val maybe_begin_local_theory: command_keyword -> string -> (local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit val local_theory': command_keyword -> string -> (bool -> local_theory -> local_theory) parser -> unit val local_theory: command_keyword -> string -> (local_theory -> local_theory) parser -> unit val local_theory_to_proof': command_keyword -> string -> (bool -> local_theory -> Proof.state) parser -> unit val local_theory_to_proof: command_keyword -> string -> (local_theory -> Proof.state) parser -> unit val bootstrap: bool Config.T val parse_spans: Token.T list -> Command_Span.span list val make_span: Token.T list -> Command_Span.span val parse_span: theory -> (unit -> theory) -> Token.T list -> Toplevel.transition val parse_text: theory -> (unit -> theory) -> Position.T -> string -> Toplevel.transition list val command_reports: theory -> Token.T -> Position.report_text list val check_command: Proof.context -> command_keyword -> string end; structure Outer_Syntax: OUTER_SYNTAX = struct (** outer syntax **) (* errors *) fun err_command msg name ps = error (msg ^ quote (Markup.markup Markup.keyword1 name) ^ Position.here_list ps); fun err_dup_command name ps = err_command "Duplicate outer syntax command " name ps; (* command parsers *) datatype command_parser = Parser of (Toplevel.transition -> Toplevel.transition) parser | Restricted_Parser of (bool * Position.T) option -> (Toplevel.transition -> Toplevel.transition) parser; datatype command = Command of {comment: string, command_parser: command_parser, pos: Position.T, id: serial}; fun eq_command (Command {id = id1, ...}, Command {id = id2, ...}) = id1 = id2; fun new_command comment command_parser pos = Command {comment = comment, command_parser = command_parser, pos = pos, id = serial ()}; fun command_pos (Command {pos, ...}) = pos; fun command_markup def (name, Command {pos, id, ...}) = Markup.properties (Position.entity_properties_of def id pos) (Markup.entity Markup.commandN name); fun pretty_command (cmd as (name, Command {comment, ...})) = Pretty.block (Pretty.marks_str ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]}, command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment); (* theory data *) structure Data = Theory_Data ( type T = command Symtab.table; val empty = Symtab.empty; val extend = I; fun merge data : T = data |> Symtab.join (fn name => fn (cmd1, cmd2) => if eq_command (cmd1, cmd2) then raise Symtab.SAME else err_dup_command name [command_pos cmd1, command_pos cmd2]); ); val get_commands = Data.get; val dest_commands = get_commands #> Symtab.dest #> sort_by #1; val lookup_commands = Symtab.lookup o get_commands; fun help thy pats = dest_commands thy |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats) |> map pretty_command |> Pretty.writeln_chunks; fun print_commands thy = let val keywords = Thy_Header.get_keywords thy; val minor = Scan.dest_lexicon (Keyword.minor_keywords keywords); val commands = dest_commands thy; in [Pretty.strs ("keywords:" :: map quote minor), Pretty.big_list "commands:" (map pretty_command commands)] |> Pretty.writeln_chunks end; (* maintain commands *) fun add_command name cmd thy = if member (op =) Thy_Header.bootstrap_thys (Context.theory_name thy) then thy else let val _ = Keyword.is_command (Thy_Header.get_keywords thy) name orelse err_command "Undeclared outer syntax command " name [command_pos cmd]; val _ = (case lookup_commands thy name of NONE => () | SOME cmd' => err_dup_command name [command_pos cmd, command_pos cmd']); val _ = Context_Position.report_generic (Context.the_generic_context ()) (command_pos cmd) (command_markup true (name, cmd)); in Data.map (Symtab.update (name, cmd)) thy end; val _ = Theory.setup (Theory.at_end (fn thy => let val command_keywords = Scan.dest_lexicon (Keyword.major_keywords (Thy_Header.get_keywords thy)); val _ = (case subtract (op =) (map #1 (dest_commands thy)) command_keywords of [] => () | missing => error ("Missing outer syntax command(s) " ^ commas_quote missing)) in NONE end)); (* implicit theory setup *) type command_keyword = string * Position.T; fun raw_command (name, pos) comment command_parser = let val setup = add_command name (new_command comment command_parser pos) in Context.>> (Context.mapping setup (Local_Theory.background_theory setup)) end; fun command (name, pos) comment parse = raw_command (name, pos) comment (Parser parse); fun maybe_begin_local_theory command_keyword comment parse_local parse_global = raw_command command_keyword comment (Restricted_Parser (fn restricted => Parse.opt_target -- parse_local >> (fn (target, f) => Toplevel.local_theory restricted target f) || (if is_some restricted then Scan.fail else parse_global >> Toplevel.begin_main_target true))); fun local_theory_command trans command_keyword comment parse = raw_command command_keyword comment (Restricted_Parser (fn restricted => Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f))); val local_theory' = local_theory_command Toplevel.local_theory'; val local_theory = local_theory_command Toplevel.local_theory; val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof'; val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof; (** toplevel parsing **) (* parse spans *) local fun ship span = let val kind = if forall Token.is_ignored span then Command_Span.Ignored_Span else if exists Token.is_error span then Command_Span.Malformed_Span else (case find_first Token.is_command span of NONE => Command_Span.Malformed_Span | SOME cmd => Command_Span.Command_Span (Token.content_of cmd, Token.pos_of cmd)); in cons (Command_Span.Span (kind, span)) end; fun flush (result, content, ignored) = result |> not (null content) ? ship (rev content) |> not (null ignored) ? ship (rev ignored); fun parse tok (result, content, ignored) = if Token.is_ignored tok then (result, content, tok :: ignored) else if Token.is_command_modifier tok orelse Token.is_command tok andalso (not (exists Token.is_command_modifier content) orelse exists Token.is_command content) then (flush (result, content, ignored), [tok], []) else (result, tok :: (ignored @ content), []); in fun parse_spans toks = fold parse toks ([], [], []) |> flush |> rev; end; fun make_span toks = (case parse_spans toks of [span] => span | _ => Command_Span.Span (Command_Span.Malformed_Span, toks)); (* parse commands *) val bootstrap = Config.declare_bool ("Outer_Syntax.bootstrap", \<^here>) (K true); local val before_command = Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false)); -fun parse_command thy core_range markers = +fun parse_command thy markers = Scan.ahead (before_command |-- Parse.position Parse.command) :|-- (fn (name, pos) => let val keywords = Thy_Header.get_keywords thy; val tr0 = Toplevel.empty |> Toplevel.name name - |> Toplevel.positions pos core_range + |> Toplevel.position pos |> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open |> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close; val command_markers = Parse.command |-- Document_Source.old_tags >> (fn tags => Toplevel.markers (map Document_Marker.legacy_tag tags @ markers) tr0); in (case lookup_commands thy name of SOME (Command {command_parser = Parser parse, ...}) => Parse.!!! (command_markers -- parse) >> (op |>) | SOME (Command {command_parser = Restricted_Parser parse, ...}) => before_command :|-- (fn restricted => Parse.!!! (command_markers -- parse restricted)) >> (op |>) | NONE => Scan.fail_with (fn _ => fn _ => let val msg = if Config.get_global thy bootstrap then "missing theory context for command " else "undefined command "; in msg ^ quote (Markup.markup Markup.keyword1 name) end)) end); in fun parse_span thy init span = let val full_range = Token.range_of span; val core_range = Token.core_range_of span; val markers = map Token.input_of (filter Token.is_document_marker span); fun parse () = filter Token.is_proper span |> Source.of_list - |> Source.source Token.stopper - (Scan.bulk (fn xs => Parse.!!! (parse_command thy core_range markers) xs)) + |> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy markers) xs)) |> Source.exhaust; in (case parse () of [tr] => Toplevel.modify_init init tr - | [] => Toplevel.ignored full_range - | _ => Toplevel.malformed core_range "Exactly one command expected") - handle ERROR msg => Toplevel.malformed core_range msg + | [] => Toplevel.ignored (#1 full_range) + | _ => Toplevel.malformed (#1 core_range) "Exactly one command expected") + handle ERROR msg => Toplevel.malformed (#1 core_range) msg end; fun parse_text thy init pos text = Symbol_Pos.explode (text, pos) |> Token.tokenize (Thy_Header.get_keywords thy) {strict = false} |> parse_spans |> map (Command_Span.content #> parse_span thy init); end; (* check commands *) fun command_reports thy tok = if Token.is_command tok then let val name = Token.content_of tok in (case lookup_commands thy name of NONE => [] | SOME cmd => [((Token.pos_of tok, command_markup false (name, cmd)), "")]) end else []; fun check_command ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val keywords = Thy_Header.get_keywords thy; in if Keyword.is_command keywords name then let val markup = Token.explode0 keywords name |> maps (command_reports thy) |> map (#2 o #1); val _ = Context_Position.reports ctxt (map (pair pos) markup); in name end else let val completion_report = Completion.make_report (name, pos) (fn completed => Keyword.dest_commands keywords |> filter completed |> sort_strings |> map (fn a => (a, (Markup.commandN, a)))); in error ("Bad command " ^ quote name ^ Position.here pos ^ completion_report) end end; (* 'ML' command -- required for bootstrapping Isar *) val _ = command ("ML", \<^here>) "ML text within theory or local theory" (Parse.ML_source >> (fn source => Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> Local_Theory.propagate_ml_env))); end; diff --git a/src/Pure/Isar/toplevel.ML b/src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML +++ b/src/Pure/Isar/toplevel.ML @@ -1,798 +1,794 @@ (* Title: Pure/Isar/toplevel.ML Author: Markus Wenzel, TU Muenchen Isabelle/Isar toplevel transactions. *) signature TOPLEVEL = sig exception UNDEF type state val init_toplevel: unit -> state val theory_toplevel: theory -> state val is_toplevel: state -> bool val is_theory: state -> bool val is_proof: state -> bool val is_skipped_proof: state -> bool val level: state -> int val previous_theory_of: state -> theory option val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory val proof_of: state -> Proof.state val proof_position_of: state -> int val is_end_theory: state -> bool val end_theory: Position.T -> state -> theory val presentation_context: state -> Proof.context val presentation_state: Proof.context -> state val pretty_context: state -> Pretty.T list val pretty_state: state -> Pretty.T list val string_of_state: state -> string val pretty_abstract: state -> Pretty.T type transition val empty: transition val name_of: transition -> string val pos_of: transition -> Position.T - val body_range_of: transition -> Position.range val timing_of: transition -> Time.time val type_error: transition -> string val name: string -> transition -> transition - val positions: Position.T -> Position.range -> transition -> transition + val position: Position.T -> transition -> transition val markers: Input.source list -> transition -> transition val timing: Time.time -> transition -> transition val init_theory: (unit -> theory) -> transition -> transition val is_init: transition -> bool val modify_init: (unit -> theory) -> transition -> transition val exit: transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val keep_proof: (state -> unit) -> transition -> transition val is_ignored: transition -> bool - val ignored: Position.range -> transition - val malformed: Position.range -> string -> transition + val ignored: Position.T -> transition + val malformed: Position.T -> string -> transition val generic_theory: (generic_theory -> generic_theory) -> transition -> transition val theory': (bool -> theory -> theory) -> transition -> transition val theory: (theory -> theory) -> transition -> transition val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition val end_main_target: transition -> transition val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition val end_nested_target: transition -> transition val local_theory': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> local_theory) -> transition -> transition val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> local_theory) -> transition -> transition val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> transition -> transition val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> Proof.state) -> transition -> transition val local_theory_to_proof: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> Proof.state) -> transition -> transition val theory_to_proof: (theory -> Proof.state) -> transition -> transition val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition val forget_proof: transition -> transition val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition val skip_proof: (unit -> unit) -> transition -> transition val skip_proof_open: transition -> transition val skip_proof_close: transition -> transition val exec_id: Document_ID.exec -> transition -> transition val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> state * (exn * string) option val command_errors: bool -> transition -> state -> Runtime.error list * state option val command_exception: bool -> transition -> state -> state val reset_theory: state -> state option val reset_proof: state -> state option val reset_notepad: state -> state option val fork_presentation: transition -> transition * transition type result val join_results: result -> (transition * state) list val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state end; structure Toplevel: TOPLEVEL = struct (** toplevel state **) exception UNDEF = Runtime.UNDEF; (* datatype node *) datatype node = Toplevel (*toplevel outside of theory body*) | Theory of generic_theory (*global or local theory*) | Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) (*proof node, finish, original theory*) | Skipped_Proof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) val theory_node = fn Theory gthy => SOME gthy | _ => NONE; val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; fun cases_node f _ _ Toplevel = f () | cases_node _ g _ (Theory gthy) = g gthy | cases_node _ _ h (Proof (prf, _)) = h (Proof_Node.current prf) | cases_node _ g _ (Skipped_Proof (_, (gthy, _))) = g gthy; fun cases_proper_node g h = cases_node (fn () => raise UNDEF) g h; val get_theory = cases_node (K NONE) (SOME o Context.theory_of) (SOME o Proof.theory_of); (* datatype state *) type node_presentation = node * Proof.context; fun init_presentation () = Proof_Context.init_global (Theory.get_pure_bootstrap ()); fun node_presentation node = (node, cases_node init_presentation Context.proof_of Proof.context_of node); datatype state = State of node_presentation * theory option; (*current node with presentation context, previous theory*) fun node_of (State ((node, _), _)) = node; fun previous_theory_of (State (_, prev_thy)) = prev_thy; fun init_toplevel () = State (node_presentation Toplevel, NONE); fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); fun level state = (case node_of state of Toplevel => 0 | Theory _ => 0 | Proof (prf, _) => Proof.level (Proof_Node.current prf) | Skipped_Proof (d, _) => d + 1); (*different notion of proof depth!*) fun str_of_state state = (case node_of state of Toplevel => (case previous_theory_of state of NONE => "at top level" | SOME thy => "at top level, result theory " ^ quote (Context.theory_name thy)) | Theory (Context.Theory _) => "in theory mode" | Theory (Context.Proof _) => "in local theory mode" | Proof _ => "in proof mode" | Skipped_Proof _ => "in skipped proof mode"); (* current node *) fun is_toplevel state = (case node_of state of Toplevel => true | _ => false); fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); fun proper_node_of state = if is_toplevel state then raise UNDEF else node_of state; fun proper_node_case f g state = cases_proper_node f g (proper_node_of state); val context_of = proper_node_case Context.proof_of Proof.context_of; val generic_theory_of = proper_node_case I (Context.Proof o Proof.context_of); val theory_of = proper_node_case Context.theory_of Proof.theory_of; val proof_of = proper_node_case (fn _ => error "No proof state") I; fun proof_position_of state = (case proper_node_of state of Proof (prf, _) => Proof_Node.position prf | _ => ~1); fun is_end_theory (State ((Toplevel, _), SOME _)) = true | is_end_theory _ = false; fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy | end_theory pos _ = error ("Malformed theory" ^ Position.here pos); (* presentation context *) structure Presentation_State = Proof_Data ( type T = state option; fun init _ = NONE; ); fun presentation_context0 (State ((_, pr_ctxt), _)) = pr_ctxt; fun presentation_context (state as State (current, _)) = presentation_context0 state |> Presentation_State.put (SOME (State (current, NONE))); fun presentation_state ctxt = (case Presentation_State.get ctxt of NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE) | SOME state => state); (* print state *) fun pretty_context state = if is_toplevel state then [] else let val gthy = (case node_of state of Toplevel => raise Match | Theory gthy => gthy | Proof (_, (_, gthy)) => gthy | Skipped_Proof (_, (_, gthy)) => gthy); val lthy = Context.cases Named_Target.theory_init I gthy; in Local_Theory.pretty lthy end; fun pretty_state state = (case node_of state of Toplevel => [] | Theory _ => [] | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf) | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of; fun pretty_abstract state = Pretty.str (""); val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract); (** toplevel transitions **) (* primitive transitions *) datatype trans = (*init theory*) Init of unit -> theory | (*formal exit of theory*) Exit | (*peek at state*) Keep of bool -> state -> unit | (*node transaction and presentation*) Transaction of (bool -> node -> node_presentation) * (state -> unit); local exception FAILURE of state * exn; fun apply f g node = let val node_pr = node_presentation node; val context = cases_proper_node I (Context.Proof o Proof.context_of) node; fun state_error e node_pr' = (State (node_pr', get_theory node), e); val (result, err) = node |> Runtime.controlled_execution (SOME context) f |> state_error NONE handle exn => state_error (SOME exn) node_pr; in (case err of NONE => tap g result | SOME exn => raise FAILURE (result, exn)) end; fun apply_tr int trans state = (case (trans, node_of state) of (Init f, Toplevel) => Runtime.controlled_execution NONE (fn () => State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = node |> apply (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) (K ()); in State ((Toplevel, pr_ctxt), get_theory node') end | (Keep f, node) => Runtime.controlled_execution (try generic_theory_of state) (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () | (Transaction _, Toplevel) => raise UNDEF | (Transaction (f, g), node) => apply (fn x => f int x) g node | _ => raise UNDEF); fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = apply_union int trs state handle Runtime.UNDEF => apply_tr int tr state | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state | exn as FAILURE _ => raise exn | exn => raise FAILURE (state, exn); fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) = let val state' = Runtime.controlled_execution (try generic_theory_of state) (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) (); in (state', NONE) end handle exn => (state, SOME exn); in fun apply_trans int name markers trans state = (apply_union int trans state |> apply_markers name markers) handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); end; (* datatype transition *) datatype transition = Transition of {name: string, (*command name*) - pos: Position.T, (*source position: reference point*) - body_range: Position.range, (*source position: main body*) + pos: Position.T, (*source position*) markers: Input.source list, (*semantic document markers*) timing: Time.time, (*prescient timing information*) trans: trans list}; (*primitive transitions (union)*) -fun make_transition (name, pos, body_range, markers, timing, trans) = - Transition {name = name, pos = pos, body_range = body_range, markers = markers, - timing = timing, trans = trans}; +fun make_transition (name, pos, markers, timing, trans) = + Transition {name = name, pos = pos, markers = markers, timing = timing, trans = trans}; -fun map_transition f (Transition {name, pos, body_range, markers, timing, trans}) = - make_transition (f (name, pos, body_range, markers, timing, trans)); +fun map_transition f (Transition {name, pos, markers, timing, trans}) = + make_transition (f (name, pos, markers, timing, trans)); -val empty = make_transition ("", Position.none, Position.no_range, [], Time.zeroTime, []); +val empty = make_transition ("", Position.none, [], Time.zeroTime, []); (* diagnostics *) fun name_of (Transition {name, ...}) = name; fun pos_of (Transition {pos, ...}) = pos; -fun body_range_of (Transition {body_range, ...}) = body_range; fun timing_of (Transition {timing, ...}) = timing; fun command_msg msg tr = msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^ Position.here (pos_of tr); fun at_command tr = command_msg "At " tr; fun type_error tr = command_msg "Bad context for " tr; (* modify transitions *) -fun name name = map_transition (fn (_, pos, body_range, markers, timing, trans) => - (name, pos, body_range, markers, timing, trans)); - -fun positions pos body_range = map_transition (fn (name, _, _, markers, timing, trans) => - (name, pos, body_range, markers, timing, trans)); +fun name name = map_transition (fn (_, pos, markers, timing, trans) => + (name, pos, markers, timing, trans)); -fun markers markers = map_transition (fn (name, pos, body_range, _, timing, trans) => - (name, pos, body_range, markers, timing, trans)); +fun position pos = map_transition (fn (name, _, markers, timing, trans) => + (name, pos, markers, timing, trans)); -fun timing timing = map_transition (fn (name, pos, body_range, markers, _, trans) => - (name, pos, body_range, markers, timing, trans)); +fun markers markers = map_transition (fn (name, pos, _, timing, trans) => + (name, pos, markers, timing, trans)); -fun add_trans tr = map_transition (fn (name, pos, body_range, markers, timing, trans) => - (name, pos, body_range, markers, timing, tr :: trans)); +fun timing timing = map_transition (fn (name, pos, markers, _, trans) => + (name, pos, markers, timing, trans)); -val reset_trans = map_transition (fn (name, pos, body_range, markers, timing, _) => - (name, pos, body_range, markers, timing, [])); +fun add_trans tr = map_transition (fn (name, pos, markers, timing, trans) => + (name, pos, markers, timing, tr :: trans)); + +val reset_trans = map_transition (fn (name, pos, markers, timing, _) => + (name, pos, markers, timing, [])); (* basic transitions *) fun init_theory f = add_trans (Init f); fun is_init (Transition {trans = [Init _], ...}) = true | is_init _ = false; fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; val exit = add_trans Exit; val keep' = add_trans o Keep; fun present_transaction f g = add_trans (Transaction (f, g)); fun transaction f = present_transaction f (K ()); fun transaction0 f = present_transaction (node_presentation oo f) (K ()); fun keep f = add_trans (Keep (fn _ => f)); fun keep_proof f = keep (fn st => if is_proof st then f st else if is_skipped_proof st then () else warning "No proof state"); fun is_ignored tr = name_of tr = ""; -fun ignored range = - empty |> name "" |> positions (#1 range) range |> keep (fn _ => ()); +fun ignored pos = + empty |> name "" |> position pos |> keep (fn _ => ()); -fun malformed range msg = - empty |> name "" |> positions (#1 range) range |> keep (fn _ => error msg); +fun malformed pos msg = + empty |> name "" |> position pos |> keep (fn _ => error msg); (* theory transitions *) fun generic_theory f = transaction (fn _ => (fn Theory gthy => node_presentation (Theory (f gthy)) | _ => raise UNDEF)); fun theory' f = transaction (fn int => (fn Theory (Context.Theory thy) => let val thy' = thy |> Sign.new_group |> f int |> Sign.reset_group; in node_presentation (Theory (Context.Theory thy')) end | _ => raise UNDEF)); fun theory f = theory' (K f); fun begin_main_target begin f = transaction (fn _ => (fn Theory (Context.Theory thy) => let val lthy = f thy; val gthy = if begin then Context.Proof lthy else Target_Context.end_named_cmd lthy; val _ = (case Local_Theory.pretty lthy of [] => () | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); in (Theory gthy, lthy) end | _ => raise UNDEF)); val end_main_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (Theory (Target_Context.end_named_cmd lthy), lthy) | _ => raise UNDEF)); fun begin_nested_target f = transaction0 (fn _ => (fn Theory gthy => let val lthy' = f gthy; in Theory (Context.Proof lthy') end | _ => raise UNDEF)); val end_nested_target = transaction (fn _ => (fn Theory (Context.Proof lthy) => (case try Target_Context.end_nested_cmd lthy of SOME gthy' => (Theory gthy', lthy) | NONE => raise UNDEF) | _ => raise UNDEF)); fun restricted_context (SOME (strict, scope)) = Proof_Context.map_naming (Name_Space.restricted strict scope) | restricted_context NONE = I; fun local_theory' restricted target f = present_transaction (fn int => (fn Theory gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val lthy' = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int |> Local_Theory.reset_group; in (Theory (finish lthy'), lthy') end | _ => raise UNDEF)) (K ()); fun local_theory restricted target f = local_theory' restricted target (K f); fun present_local_theory target = present_transaction (fn _ => (fn Theory gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; in (Theory (finish lthy), lthy) end | _ => raise UNDEF)); (* proof transitions *) fun end_proof f = transaction (fn int => (fn Proof (prf, (finish, _)) => let val state = Proof_Node.current prf in if can (Proof.assert_bottom true) state then let val ctxt' = f int state; val gthy' = finish ctxt'; in (Theory gthy', ctxt') end else raise UNDEF end | Skipped_Proof (0, (gthy, _)) => node_presentation (Theory gthy) | _ => raise UNDEF)); local fun begin_proof init_proof = transaction0 (fn int => (fn Theory gthy => let val (finish, prf) = init_proof int gthy; val document = Options.default_string "document"; val skip = (document = "" orelse document = "false") andalso Goal.skip_proofs_enabled (); val schematic_goal = try Proof.schematic_goal prf; val _ = if skip andalso schematic_goal = SOME true then warning "Cannot skip proof of schematic goal statement" else (); in if skip andalso schematic_goal = SOME false then Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) else Proof (Proof_Node.init prf, (finish, gthy)) end | _ => raise UNDEF)); in fun local_theory_to_proof' restricted target f = begin_proof (fn int => fn gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; val prf = lthy |> restricted_context restricted |> Local_Theory.new_group |> f int; in (finish o Local_Theory.reset_group, prf) end); fun local_theory_to_proof restricted target f = local_theory_to_proof' restricted target (K f); fun theory_to_proof f = begin_proof (fn _ => fn gthy => (Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, (case gthy of Context.Theory thy => f (Sign.new_group thy) | _ => raise UNDEF))); end; val forget_proof = transaction0 (fn _ => (fn Proof (prf, (_, orig_gthy)) => if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF else Theory orig_gthy | Skipped_Proof (_, (_, orig_gthy)) => Theory orig_gthy | _ => raise UNDEF)); fun proofs' f = transaction0 (fn int => (fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) | skip as Skipped_Proof _ => skip | _ => raise UNDEF)); fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); val proofs = proofs' o K; val proof = proof' o K; (* skipped proofs *) fun actual_proof f = transaction0 (fn _ => (fn Proof (prf, x) => Proof (f prf, x) | _ => raise UNDEF)); fun skip_proof f = transaction0 (fn _ => (fn skip as Skipped_Proof _ => (f (); skip) | _ => raise UNDEF)); val skip_proof_open = transaction0 (fn _ => (fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x) | _ => raise UNDEF)); val skip_proof_close = transaction0 (fn _ => (fn Skipped_Proof (0, (gthy, _)) => Theory gthy | Skipped_Proof (d, x) => Skipped_Proof (d - 1, x) | _ => raise UNDEF)); (** toplevel transactions **) (* runtime position *) -fun exec_id id (tr as Transition {pos, body_range, ...}) = +fun exec_id id (tr as Transition {pos, ...}) = let val put_id = Position.put_id (Document_ID.print id) - in positions (put_id pos) (apply2 put_id body_range) tr end; + in position (put_id pos) tr end; fun setmp_thread_position (Transition {pos, ...}) f x = Position.setmp_thread_data pos f x; (* post-transition hooks *) local val hooks = Synchronized.var "Toplevel.hooks" ([]: (transition -> state -> state -> unit) list); in fun add_hook hook = Synchronized.change hooks (cons hook); fun get_hooks () = Synchronized.value hooks; end; (* apply transitions *) local fun app int (tr as Transition {name, markers, trans, ...}) = setmp_thread_position tr (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans) ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)); in fun transition int tr st = let val (st', opt_err) = Context.setmp_generic_context (try (Context.Proof o presentation_context0) st) (fn () => app int tr st) (); val opt_err' = opt_err |> Option.map (fn Runtime.EXCURSION_FAIL exn_info => exn_info | exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ())); in (st', opt_err') end; end; (* managed commands *) fun command_errors int tr st = (case transition int tr st of (st', NONE) => ([], SOME st') | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE)); fun command_exception int tr st = (case transition int tr st of (st', NONE) => st' | (_, SOME (exn, info)) => if Exn.is_interrupt exn then Exn.reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)); val command = command_exception false; (* reset state *) local fun reset_state check trans st = if check st then NONE else #2 (command_errors false (trans empty) st); in val reset_theory = reset_state is_theory forget_proof; val reset_proof = reset_state is_proof (transaction0 (fn _ => (fn Theory gthy => Skipped_Proof (0, (gthy, gthy)) | _ => raise UNDEF))); val reset_notepad = reset_state (fn st => (case try proof_of st of SOME state => not (Proof.is_notepad state) orelse can Proof.end_notepad state | NONE => true)) (proof Proof.reset_notepad); end; (* scheduled proof result *) datatype result = Result of transition * state | Result_List of result list | Result_Future of result future; fun join_results (Result x) = [x] | join_results (Result_List xs) = maps join_results xs | join_results (Result_Future x) = join_results (Future.join x); local structure Result = Proof_Data ( type T = result; fun init _ = Result_List []; ); val get_result = Result.get o Proof.context_of; val put_result = Proof.map_context o Result.put; fun timing_estimate elem = let val trs = tl (Thy_Element.flat_element elem) in fold (fn tr => fn t => timing_of tr + t) trs Time.zeroTime end; fun future_proofs_enabled estimate st = (case try proof_of st of NONE => false | SOME state => not (Proofterm.proofs_enabled ()) andalso not (Proof.is_relevant state) andalso (if can (Proof.assert_bottom true) state then Future.proofs_enabled 1 else Future.proofs_enabled 2 orelse Future.proofs_enabled_timing estimate)); val empty_markers = markers []; val empty_trans = reset_trans #> keep (K ()); in fun fork_presentation tr = (tr |> empty_markers, tr |> empty_trans); fun atom_result keywords tr st = let val st' = if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then let val (tr1, tr2) = fork_presentation tr; val _ = Execution.fork {name = "Toplevel.diag", pos = pos_of tr, pri = ~1} (fn () => command tr1 st); in command tr2 st end else command tr st; in (Result (tr, st'), st') end; fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st = let val (head_result, st') = atom_result keywords head_tr st; val (body_elems, end_tr) = element_rest; val estimate = timing_estimate elem; in if not (future_proofs_enabled estimate st') then let val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr]; val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; in (Result_List (head_result :: proof_results), st'') end else let val (end_tr1, end_tr2) = fork_presentation end_tr; val finish = Context.Theory o Proof_Context.theory_of; val future_proof = Proof.future_proof (fn state => Execution.fork {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} (fn () => let val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st'; val node' = Proof (Proof_Node.apply (K state) prf, (finish, orig_gthy)); val (results, result_state) = State (node_presentation node', prev_thy) |> fold_map (element_result keywords) body_elems ||> command end_tr1; in (Result_List results, presentation_context0 result_state) end)) #> (fn (res, state') => state' |> put_result (Result_Future res)); val forked_proof = proof (future_proof #> (fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o end_proof (fn _ => future_proof #> (fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); val st'' = st' |> command (head_tr |> reset_trans |> forked_proof); val end_st = st'' |> command end_tr2; val end_result = Result (end_tr, end_st); val result = Result_List [head_result, Result.get (presentation_context0 st''), end_result]; in (result, end_st) end end; end; 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,509 +1,507 @@ (* Title: Pure/PIDE/command.ML Author: Makarius Prover command execution: read -- eval -- print. *) signature COMMAND = sig type blob = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option} val read_file: Path.T -> Position.T -> bool -> Path.T -> Token.file val read_thy: Toplevel.state -> theory val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> blob Exn.result list * int -> Token.T list -> Toplevel.transition val read_span: Keyword.keywords -> Toplevel.state -> Path.T -> (unit -> theory) -> Command_Span.span -> 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 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 = {file_node: string, src_path: Path.T, content: (SHA1.digest * string list) option}; fun read_file_node file_node master_dir pos delimited src_path = let val _ = if Context_Position.pide_reports () then Position.report pos (Markup.language_path delimited) else (); fun read_file () = let val path = File.check_file (File.full_path master_dir src_path); val text = File.read path; val file_pos = Path.position path; in (text, file_pos) end; fun read_url () = let val text = Isabelle_System.download file_node; val file_pos = Position.file file_node; in (text, file_pos) end; val (text, file_pos) = (case try Url.explode file_node of NONE => read_file () | SOME (Url.File _) => read_file () | _ => read_url ()); val lines = split_lines text; val digest = SHA1.digest text; in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id 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 master_dir (blobs, blobs_index) toks = (case Outer_Syntax.parse_spans toks of [Command_Span.Span (Command_Span.Command_Span _, _)] => (case try (nth toks) blobs_index of SOME tok => let val source = Token.input_of tok; val pos = Input.pos_of source; val delimited = Input.is_delimited source; fun make_file (Exn.Res {file_node, src_path, content = NONE}) = Exn.interruptible_capture (fn () => read_file_node file_node master_dir pos delimited src_path) () | make_file (Exn.Res {file_node, src_path, content = SOME (digest, lines)}) = (Position.report pos (Markup.language_path delimited); Exn.Res (blob_file src_path lines digest file_node)) | 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 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 (Token.core_range_of span) "Malformed command syntax" + then Toplevel.malformed (#1 (Token.core_range_of span)) "Malformed command syntax" else Outer_Syntax.parse_span thy init (resolve_files master_dir blobs_info span) end; end; fun read_span keywords st master_dir init = Command_Span.content #> read keywords (read_thy st) master_dir init ([], ~1); (* 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_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 (Thm.nprems_of o #goal o Proof.goal) prf of NONE => () | SOME 0 => () | SOME n => - let - val pos = #1 (Toplevel.body_range_of tr); - val m = Markup.command_indent (n - 1); - in Toplevel.setmp_thread_position tr (fn () => Position.report pos m) () end) + let val report = Markup.markup_only (Markup.command_indent (n - 1)); + in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end) else () end | NONE => ()); fun status tr m = Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) (); fun eval_state keywords span tr ({state, ...}: eval_state) = let val _ = Thread_Attributes.expose_interrupt (); val st = reset_state keywords tr state; val _ = report_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/Tools/jEdit/src/text_structure.scala b/src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala +++ b/src/Tools/jEdit/src/text_structure.scala @@ -1,353 +1,354 @@ /* Title: Tools/jEdit/src/text_structure.scala Author: Makarius Text structure based on Isabelle/Isar outer syntax. */ package isabelle.jedit import isabelle._ import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.Buffer object Text_Structure { /* token navigator */ class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean) { val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } } /* indentation */ object Indent_Rule extends IndentRule { private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open private val keyword_close = Keyword.proof_close def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int, actions: java.util.List[IndentAction]) { Isabelle.buffer_syntax(buffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, true) val indent_size = buffer.getIndentSize def line_indent(line: Int): Int = if (line < 0 || line >= buffer.getLineCount) 0 else buffer.getCurrentIndentForLine(line, null) def line_head(line: Int): Option[Text.Info[Token]] = nav.iterator(line, 1).toStream.headOption def head_is_quasi_command(line: Int): Boolean = line_head(line) match { case None => false case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok) } val prev_line: Int = Range.inclusive(current_line - 1, 0, -1).find(line => Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && (!Token_Markup.Line_Context.after(buffer, line).structure.improper || Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1 def prev_line_command: Option[Token] = nav.reverse_iterator(prev_line, 1). collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) def prev_line_span: Iterator[Token] = nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command) def prev_span: Iterator[Token] = nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) val script_indent: Text.Info[Token] => Int = { val opt_rendering: Option[JEdit_Rendering] = if (PIDE.options.value.bool("jedit_indent_script")) GUI_Thread.now { (for { text_area <- JEdit_Lib.jedit_text_areas(buffer) doc_view <- Document_View.get(text_area) } yield doc_view.get_rendering).toStream.headOption } else None val limit = PIDE.options.value.int("jedit_indent_script_limit") (info: Text.Info[Token]) => opt_rendering match { case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) => (rendering.indentation(info.range) min limit) max 0 case _ => 0 } } def indent_indent(tok: Token): Int = if (keywords.is_command(tok, keyword_open)) indent_size else if (keywords.is_command(tok, keyword_close)) - indent_size else 0 def indent_offset(tok: Token): Int = if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size else 0 def indent_structure: Int = nav.reverse_iterator(current_line - 1).scanLeft((0, false))( { case ((ind, _), Text.Info(range, tok)) => val ind1 = ind + indent_indent(tok) if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) { val line = buffer.getLineOfOffset(range.start) line_head(line) match { case Some(info) if info.info == tok => (ind1 + indent_offset(tok) + line_indent(line), true) case _ => (ind1, false) } } else (ind1, false) }).collectFirst({ case (i, true) => i }).getOrElse(0) def indent_brackets: Int = (0 /: prev_line_span)( { case (i, tok) => if (tok.is_open_bracket) i + indent_size else if (tok.is_close_bracket) i - indent_size else i }) def indent_extra: Int = if (prev_span.exists(keywords.is_quasi_command)) indent_size else 0 val indent = if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished) line_indent(current_line) else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0 else { line_head(current_line) match { - case Some(info @ Text.Info(range, tok)) => + case Some(info) => + val tok = info.info if (tok.is_begin || keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory)) 0 else if (keywords.is_command(tok, Keyword.proof_enclose)) indent_structure + script_indent(info) - indent_offset(tok) else if (keywords.is_command(tok, Keyword.proof)) (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size else if (tok.is_command) indent_structure - indent_offset(tok) else { prev_line_command match { case None => val extra = (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { case (true, true) | (false, false) => 0 case (true, false) => - indent_extra case (false, true) => indent_extra } line_indent(prev_line) + indent_brackets + extra - indent_offset(tok) case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(tok) - indent_offset(prev_tok) - indent_indent(prev_tok) } } case None => prev_line_command match { case None => val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0 line_indent(prev_line) + indent_brackets + extra case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(prev_tok) - indent_indent(prev_tok) } } } actions.clear() actions.add(new IndentAction.AlignOffset(indent max 0)) case None => } } } def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) = { val text = JEdit_Lib.get_text(buffer, range).getOrElse("") val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt) val toks1 = toks.filterNot(_.is_space) (toks1, ctxt1) } def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int) : (List[Token], List[Token]) = { val line_range = JEdit_Lib.line_range(buffer, line) val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0) val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1) (toks1, toks2) } /* structure matching */ object Matcher extends StructureMatcher { private def find_block( open: Token => Boolean, close: Token => Boolean, reset: Token => Boolean, restrict: Token => Boolean, it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = { val range1 = it.next.range it.takeWhile(info => !info.info.is_command || restrict(info.info)). scanLeft((range1, 1))( { case ((r, d), Text.Info(range, tok)) => if (open(tok)) (range, d + 1) else if (close(tok)) (range, d - 1) else if (reset(tok)) (range, 0) else (r, d) } ).collectFirst({ case (range2, 0) => (range1, range2) }) } private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = { val buffer = text_area.getBuffer val caret_line = text_area.getCaretLine val caret = text_area.getCaretPosition Isabelle.buffer_syntax(text_area.getBuffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, false) def caret_iterator(): Iterator[Text.Info[Token]] = nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) def reverse_caret_iterator(): Iterator[Text.Info[Token]] = nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) match { case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), keywords.is_command(_, Keyword.qed_global), t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) case _ => None } case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) => find_block( keywords.is_command(_, Keyword.qed), t => keywords.is_command(t, Keyword.proof_goal) || keywords.is_command(t, Keyword.theory_goal), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof) || keywords.is_command(t, Keyword.theory_goal), reverse_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_end => find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) match { case Some((_, range2)) => reverse_caret_iterator(). dropWhile(info => info.range != range2). dropWhile(info => info.range == range2). find(info => info.info.is_command || info.info.is_begin) match { case Some(Text.Info(range3, tok)) => if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3)) else Some((range1, range2)) case None => None } case None => None } case _ => None } case None => None } } def getMatch(text_area: TextArea): StructureMatcher.Match = find_pair(text_area) match { case Some((_, range)) => val line = text_area.getBuffer.getLineOfOffset(range.start) new StructureMatcher.Match(Matcher, line, range.start, line, range.stop) case None => null } def selectMatch(text_area: TextArea) { def get_span(offset: Text.Offset): Option[Text.Range] = for { syntax <- Isabelle.buffer_syntax(text_area.getBuffer) span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) } yield span.range find_pair(text_area) match { case Some((r1, r2)) => (get_span(r1.start), get_span(r2.start)) match { case (Some(range1), Some(range2)) => val start = range1.start min range2.start val stop = range1.stop max range2.stop text_area.moveCaretPosition(stop, false) if (!text_area.isMultipleSelectionEnabled) text_area.selectNone text_area.addToSelection(new Selection.Range(start, stop)) case _ => } case None => } } } }