# HG changeset patch
# User wenzelm
# Date 1754992578 -7200
# Node ID 3300a2aadc3aa08d6035352d031f7dd7345c9b0d
# Parent  947d10dbe353dee7559f7a077978044303380fc7
discontinue odd test for obsolete manual (see also 2288a6f17930);

diff -r 947d10dbe353 -r 3300a2aadc3a src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Aug 12 11:32:05 2025 +0200
+++ b/src/Doc/ROOT	Tue Aug 12 11:56:18 2025 +0200
@@ -388,8 +388,6 @@
     "Inductive" "Misc" "Protocol" "Rules" "Sets" "ToyList" "Trie" "Types"
   theories [document = false]
     Base
-  theories [threads = 1]
-    "ToyList/ToyList_Test"
   theories [thy_output_indent = 5]
     "ToyList/ToyList"
     "Ifexpr/Ifexpr"
diff -r 947d10dbe353 -r 3300a2aadc3a src/Doc/Tutorial/ToyList/ToyList_Test.thy
--- a/src/Doc/Tutorial/ToyList/ToyList_Test.thy	Tue Aug 12 11:32:05 2025 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-theory ToyList_Test
-imports Main
-begin
-
-ML \<open>
-  let val text =
-    map (File.read o Path.append \<^master_dir>) [\<^path>\<open>ToyList1.txt\<close>, \<^path>\<open>ToyList2.txt\<close>]
-    |> implode
-  in Thy_Info.script_thy Position.start text \<^theory> end
-\<close>
-
-end
diff -r 947d10dbe353 -r 3300a2aadc3a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Aug 12 11:32:05 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Aug 12 11:56:18 2025 +0200
@@ -25,7 +25,6 @@
   val use_theories: Options.T -> string -> (string * Position.T) list ->
     (theory * Document_Output.segment list) list
   val use_thy: string -> unit
-  val script_thy: Position.T -> string -> theory -> theory
   val finish: unit -> unit
 end;
 
@@ -463,16 +462,6 @@
   ignore (use_theories (Options.default ()) Resources.default_qualifier [(name, Position.none)]);
 
 
-(* toplevel scripting -- without maintaining database *)
-
-fun script_thy pos txt thy =
-  let
-    val trs = Outer_Syntax.parse_text thy (K thy) 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.make_state NONE);
-  in Toplevel.end_theory end_pos end_state end;
-
-
 (* finish all theories *)
 
 fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));