1.1 --- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Wed Jul 23 21:01:28 2014 +0200
     1.2 +++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Wed Jul 23 21:02:45 2014 +0200
     1.3 @@ -2,14 +2,11 @@
     1.4  imports Datatype
     1.5  begin
     1.6  
     1.7 -ML {*  (* FIXME somewhat non-standard, fragile *)
     1.8 -  let
     1.9 -    val texts =
    1.10 -      map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
    1.11 -        ["ToyList1.txt", "ToyList2.txt"];
    1.12 -    val trs = Outer_Syntax.parse Position.start (implode texts);
    1.13 -    val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
    1.14 -  in @{assert} (Toplevel.is_toplevel end_state) end;
    1.15 +ML {*
    1.16 +  map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
    1.17 +    ["ToyList1.txt", "ToyList2.txt"]
    1.18 +  |> implode
    1.19 +  |> Thy_Info.script_thy Position.start
    1.20  *}
    1.21  
    1.22  end

     2.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jul 23 21:01:28 2014 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 23 21:02:45 2014 +0200
     2.3 @@ -22,6 +22,7 @@
     2.4      (string * Position.T) list -> unit
     2.5    val use_thys: (string * Position.T) list -> unit
     2.6    val use_thy: string * Position.T -> unit
     2.7 +  val script_thy: Position.T -> string -> theory
     2.8    val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
     2.9    val register_thy: theory -> unit
    2.10    val finish: unit -> unit
    2.11 @@ -375,7 +376,14 @@
    2.12  val use_thy = use_thys o single;
    2.13  
    2.14  
    2.15 -(* toplevel begin theory -- without maintaining database *)
    2.16 +(* toplevel scripting -- without maintaining database *)
    2.17 +
    2.18 +fun script_thy pos txt =
    2.19 +  let
    2.20 +    val trs = Outer_Syntax.parse pos txt;
    2.21 +    val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
    2.22 +    val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
    2.23 +  in Toplevel.end_theory end_pos end_state end;
    2.24  
    2.25  fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
    2.26    let