run_command: check theory name for init;
authorwenzelm
Fri Jan 16 15:20:31 2009 +0100 (2009-01-16 ago)
changeset 2951638b68c7ce621
parent 29515 53bda11e0d3b
child 29517 d7648f30f923
run_command: check theory name for init;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Jan 16 15:20:05 2009 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Jan 16 15:20:31 2009 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4    val transition: bool -> transition -> state -> (state * (exn * string) option) option
     1.5    val commit_exit: Position.T -> transition
     1.6    val command: transition -> state -> state
     1.7 -  val run_command: transition -> state -> state option
     1.8 +  val run_command: string -> transition -> state -> state option
     1.9    val excursion: (transition * transition list) list -> (transition * state) list lazy
    1.10  end;
    1.11  
    1.12 @@ -698,11 +698,17 @@
    1.13    let val st' = command tr st
    1.14    in (st', st') end;
    1.15  
    1.16 -fun run_command tr st =
    1.17 -  (case transition true tr st of
    1.18 -    SOME (st', NONE) => (status tr Markup.finished; SOME st')
    1.19 -  | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.20 -  | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE));
    1.21 +fun run_command thy_name tr st =
    1.22 +  (case
    1.23 +      (case init_of tr of
    1.24 +        SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) ()
    1.25 +      | NONE => Exn.Result ()) of
    1.26 +    Exn.Result () =>
    1.27 +      (case transition true tr st of
    1.28 +        SOME (st', NONE) => (status tr Markup.finished; SOME st')
    1.29 +      | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE)
    1.30 +      | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE))
    1.31 +  | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE));
    1.32  
    1.33  
    1.34  (* excursion of units, consisting of commands with proof *)