1.1 --- a/src/Pure/PIDE/command.ML	Wed Jul 03 15:19:36 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Jul 03 16:19:57 2013 +0200
     1.3 @@ -6,21 +6,26 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  val range: Token.T list -> Position.range
     1.8 -  val proper_range: Token.T list -> Position.range
     1.9 +  type span = Token.T list
    1.10 +  val range: span -> Position.range
    1.11 +  val proper_range: span -> Position.range
    1.12    type 'a memo
    1.13    val memo: (unit -> 'a) -> 'a memo
    1.14    val memo_value: 'a -> 'a memo
    1.15    val memo_eval: 'a memo -> 'a
    1.16    val memo_result: 'a memo -> 'a
    1.17 -  val run_command: Toplevel.transition * Token.T list ->
    1.18 -    Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy
    1.19 +  val eval: span -> Toplevel.transition ->
    1.20 +    Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    1.21 +  val no_print: unit lazy
    1.22 +  val print: Toplevel.transition -> Toplevel.state -> unit lazy
    1.23  end;
    1.24  
    1.25  structure Command: COMMAND =
    1.26  struct
    1.27  
    1.28 -(* span range *)
    1.29 +(* source *)
    1.30 +
    1.31 +type span = Token.T list;
    1.32  
    1.33  val range = Token.position_range_of;
    1.34  val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    1.35 @@ -57,7 +62,30 @@
    1.36  end;
    1.37  
    1.38  
    1.39 -(* run command *)
    1.40 +(* side-comments *)
    1.41 +
    1.42 +local
    1.43 +
    1.44 +fun cmts (t1 :: t2 :: toks) =
    1.45 +      if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
    1.46 +      else cmts (t2 :: toks)
    1.47 +  | cmts _ = [];
    1.48 +
    1.49 +val span_cmts = filter Token.is_proper #> cmts;
    1.50 +
    1.51 +in
    1.52 +
    1.53 +fun check_cmts span tr st' =
    1.54 +  Toplevel.setmp_thread_position tr
    1.55 +    (fn () =>
    1.56 +      span_cmts span |> maps (fn cmt =>
    1.57 +        (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    1.58 +          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    1.59 +
    1.60 +end;
    1.61 +
    1.62 +
    1.63 +(* eval *)
    1.64  
    1.65  local
    1.66  
    1.67 @@ -67,28 +95,16 @@
    1.68        (fn () => Toplevel.command_exception int tr st); ([], SOME st))
    1.69    else Toplevel.command_errors int tr st;
    1.70  
    1.71 -fun check_cmts tr cmts st =
    1.72 -  Toplevel.setmp_thread_position tr
    1.73 -    (fn () => cmts
    1.74 -      |> maps (fn cmt =>
    1.75 -        (Thy_Output.check_text (Token.source_position_of cmt) st; [])
    1.76 -          handle exn => ML_Compiler.exn_messages_ids exn)) ();
    1.77 -
    1.78  fun proof_status tr st =
    1.79    (case try Toplevel.proof_of st of
    1.80      SOME prf => Toplevel.status tr (Proof.status_markup prf)
    1.81    | NONE => ());
    1.82  
    1.83 -val no_print = Lazy.value ();
    1.84 -
    1.85 -fun print_state tr st =
    1.86 -  (Lazy.lazy o Toplevel.setmp_thread_position tr)
    1.87 -    (fn () => Toplevel.print_state false st);
    1.88 -
    1.89  in
    1.90  
    1.91 -fun run_command (tr, cmts) (st, malformed) =
    1.92 -  if malformed then ((Toplevel.toplevel, malformed), no_print)
    1.93 +fun eval span tr (st, {malformed}) =
    1.94 +  if malformed then
    1.95 +    ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
    1.96    else
    1.97      let
    1.98        val malformed' = Toplevel.is_malformed tr;
    1.99 @@ -98,7 +114,7 @@
   1.100        val _ = Multithreading.interrupted ();
   1.101        val _ = Toplevel.status tr Markup.running;
   1.102        val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   1.103 -      val errs2 = (case result of NONE => [] | SOME st' => check_cmts tr cmts st');
   1.104 +      val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   1.105        val errs = errs1 @ errs2;
   1.106        val _ = Toplevel.status tr Markup.finished;
   1.107        val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   1.108 @@ -108,17 +124,33 @@
   1.109            let
   1.110              val _ = if null errs then Exn.interrupt () else ();
   1.111              val _ = Toplevel.status tr Markup.failed;
   1.112 -          in ((st, malformed'), no_print) end
   1.113 +          in ({failed = true}, (st, {malformed = malformed'})) end
   1.114        | SOME st' =>
   1.115            let
   1.116              val _ = proof_status tr st';
   1.117 -            val do_print =
   1.118 -              not is_init andalso
   1.119 -                (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   1.120 -          in ((st', malformed'), if do_print then print_state tr st' else no_print) end)
   1.121 +          in ({failed = false}, (st', {malformed = malformed'})) end)
   1.122      end;
   1.123  
   1.124  end;
   1.125  
   1.126 +
   1.127 +(* print *)
   1.128 +
   1.129 +val no_print = Lazy.value ();
   1.130 +
   1.131 +fun print tr st' =
   1.132 +  let
   1.133 +    val is_init = Toplevel.is_init tr;
   1.134 +    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   1.135 +    val do_print =
   1.136 +      not is_init andalso
   1.137 +        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   1.138 +  in
   1.139 +    if do_print then
   1.140 +      (Lazy.lazy o Toplevel.setmp_thread_position tr)
   1.141 +        (fn () => Toplevel.print_state false st')
   1.142 +    else no_print
   1.143 +  end;
   1.144 +
   1.145  end;
   1.146