# HG changeset patch
# User wenzelm
# Date 1406142165 -7200
# Node ID 2288a6f17930bae19f786204f01d39bcb629413c
# Parent  2a9d8dcea893fc4c30008b6609adaae782d1821f
more official Thy_Info.script_thy;

diff -r 2a9d8dcea893 -r 2288a6f17930 src/Doc/Tutorial/ToyList/ToyList_Test.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
diff -r 2a9d8dcea893 -r 2288a6f17930 src/Pure/Thy/thy_info.ML
--- 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