--- 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"
--- 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
--- 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)));