--- 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