more official Thy_Info.script_thy;

--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Wed Jul 23 21:01:28 2014 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Wed Jul 23 21:02:45 2014 +0200
@@ -2,14 +2,11 @@
 imports Datatype
 begin
 
-ML {*  (* FIXME somewhat non-standard, fragile *)
-  let
-    val texts =
-      map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
-        ["ToyList1.txt", "ToyList2.txt"];
-    val trs = Outer_Syntax.parse Position.start (implode texts);
-    val end_state = fold (Toplevel.command_exception false) trs Toplevel.toplevel;
-  in @{assert} (Toplevel.is_toplevel end_state) end;
+ML {*
+  map (File.read o Path.append (Resources.master_directory @{theory}) o Path.explode)
+    ["ToyList1.txt", "ToyList2.txt"]
+  |> implode
+  |> Thy_Info.script_thy Position.start
 *}
 
 end

--- a/src/Pure/Thy/thy_info.ML	Wed Jul 23 21:01:28 2014 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jul 23 21:02:45 2014 +0200
@@ -22,6 +22,7 @@
     (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
+  val script_thy: Position.T -> string -> theory
   val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
@@ -375,7 +376,14 @@
 val use_thy = use_thys o single;
 
 
-(* toplevel begin theory -- without maintaining database *)
+(* toplevel scripting -- without maintaining database *)
+
+fun script_thy pos txt =
+  let
+    val trs = Outer_Syntax.parse pos txt;
+    val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs);
+    val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel;
+  in Toplevel.end_theory end_pos end_state end;
 
 fun toplevel_begin_theory master_dir (header: Thy_Header.header) =
   let