# HG changeset patch # User wenzelm # Date 1333541987 -7200 # Node ID bed4b2738d8a01e112a7f2058323321001d9884b # Parent 693276dcc51228dd16a5c0cdc19fe36b12dd93ed separate module for prover command execution; diff -r 693276dcc512 -r bed4b2738d8a src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Apr 04 14:00:47 2012 +0200 +++ b/src/Pure/IsaMakefile Wed Apr 04 14:19:47 2012 +0200 @@ -155,6 +155,7 @@ ML/ml_parse.ML \ ML/ml_syntax.ML \ ML/ml_thms.ML \ + PIDE/command.ML \ PIDE/document.ML \ PIDE/isabelle_markup.ML \ PIDE/markup.ML \ diff -r 693276dcc512 -r bed4b2738d8a src/Pure/PIDE/command.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/command.ML Wed Apr 04 14:19:47 2012 +0200 @@ -0,0 +1,85 @@ +(* Title: Pure/PIDE/command.ML + Author: Makarius + +Prover command execution. +*) + +signature COMMAND = +sig + val parse_command: string -> string -> Token.T list + val run_command: Toplevel.transition -> Toplevel.state -> Toplevel.state * unit lazy +end; + +structure Command: COMMAND = +struct + +(* parse *) + +fun parse_command id text = + Position.setmp_thread_data (Position.id_only id) + (fn () => + let + val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text; + val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed); + in toks end) (); + + +(* run *) + +local + +fun run int tr st = + (case Toplevel.transition int tr st of + SOME (st', NONE) => ([], SOME st') + | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) + | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); + +fun timing tr t = + if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); + +fun proof_status tr st = + (case try Toplevel.proof_of st of + SOME prf => Toplevel.status tr (Proof.status_markup prf) + | NONE => ()); + +val no_print = Lazy.value (); + +fun print_state tr st = + (Lazy.lazy o Toplevel.setmp_thread_position tr) + (fn () => Toplevel.print_state false st); + +in + +fun run_command tr st = + let + val is_init = Toplevel.is_init tr; + val is_proof = Keyword.is_proof (Toplevel.name_of tr); + + val _ = Multithreading.interrupted (); + val _ = Toplevel.status tr Isabelle_Markup.forked; + val start = Timing.start (); + val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; + val _ = timing tr (Timing.result start); + val _ = Toplevel.status tr Isabelle_Markup.joined; + val _ = List.app (Toplevel.error_msg tr) errs; + in + (case result of + NONE => + let + val _ = if null errs then Exn.interrupt () else (); + val _ = Toplevel.status tr Isabelle_Markup.failed; + in (st, no_print) end + | SOME st' => + let + val _ = Toplevel.status tr Isabelle_Markup.finished; + val _ = proof_status tr st'; + val do_print = + not is_init andalso + (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); + in (st', if do_print then print_state tr st' else no_print) end) + end; + +end; + +end; + diff -r 693276dcc512 -r bed4b2738d8a src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Wed Apr 04 14:00:47 2012 +0200 +++ b/src/Pure/PIDE/document.ML Wed Apr 04 14:19:47 2012 +0200 @@ -63,8 +63,7 @@ structure Entries = Linear_Set(type key = command_id val ord = int_ord); type exec = exec_id * (Toplevel.state * unit lazy) lazy; (*eval/print process*) -val no_print = Lazy.value (); -val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print)); +val no_exec = (no_id, Lazy.value (Toplevel.toplevel, Lazy.value ())); abstype node = Node of {touched: bool, @@ -276,18 +275,10 @@ (* commands *) -fun parse_command id text = - Position.setmp_thread_data (Position.id_only id) - (fn () => - let - val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text; - val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed); - in toks end) (); - fun define_command (id: command_id) name text = map_state (fn (versions, commands, execution) => let - val span = Lazy.lazy (fn () => parse_command (print_id id) text); + val span = Lazy.lazy (fn () => Command.parse_command (print_id id) text); val commands' = Inttab.update_new (id, (name, span)) commands handle Inttab.DUP dup => err_dup "command" dup; @@ -306,62 +297,6 @@ end; -(* toplevel transactions *) - -local - -fun run int tr st = - (case Toplevel.transition int tr st of - SOME (st', NONE) => ([], SOME st') - | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) - | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); - -fun timing tr t = - if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); - -fun proof_status tr st = - (case try Toplevel.proof_of st of - SOME prf => Toplevel.status tr (Proof.status_markup prf) - | NONE => ()); - -fun print_state tr st = - (Lazy.lazy o Toplevel.setmp_thread_position tr) - (fn () => Toplevel.print_state false st); - -in - -fun run_command tr st = - let - val is_init = Toplevel.is_init tr; - val is_proof = Keyword.is_proof (Toplevel.name_of tr); - - val _ = Multithreading.interrupted (); - val _ = Toplevel.status tr Isabelle_Markup.forked; - val start = Timing.start (); - val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; - val _ = timing tr (Timing.result start); - val _ = Toplevel.status tr Isabelle_Markup.joined; - val _ = List.app (Toplevel.error_msg tr) errs; - in - (case result of - NONE => - let - val _ = if null errs then Exn.interrupt () else (); - val _ = Toplevel.status tr Isabelle_Markup.failed; - in (st, no_print) end - | SOME st' => - let - val _ = Toplevel.status tr Isabelle_Markup.finished; - val _ = proof_status tr st'; - val do_print = - not is_init andalso - (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); - in (st', if do_print then print_state tr st' else no_print) end) - end; - -end; - - (** update **) @@ -454,7 +389,8 @@ #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) |> modify_init |> Toplevel.put_id exec_id'_string); - val exec' = snd (snd command_exec) |> Lazy.map (fn (st, _) => run_command (tr ()) st); + val exec' = + snd (snd command_exec) |> Lazy.map (fn (st, _) => Command.run_command (tr ()) st); val command_exec' = (command_id', (exec_id', exec')); in SOME (command_exec' :: execs, command_exec', init') end; diff -r 693276dcc512 -r bed4b2738d8a src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Apr 04 14:00:47 2012 +0200 +++ b/src/Pure/ROOT.ML Wed Apr 04 14:19:47 2012 +0200 @@ -251,6 +251,7 @@ use "Thy/present.ML"; use "Thy/thy_load.ML"; use "Thy/thy_info.ML"; +use "PIDE/command.ML"; use "PIDE/document.ML"; use "Thy/rail.ML";