Fri, 26 Aug 2022 21:25:35 +0200 tuned whitespace;
wenzelm [Fri, 26 Aug 2022 21:25:35 +0200] rev 75985
tuned whitespace;
Fri, 26 Aug 2022 12:44:06 +0200 tuned signature;
wenzelm [Fri, 26 Aug 2022 12:44:06 +0200] rev 75984
tuned signature;
Fri, 26 Aug 2022 12:38:00 +0200 removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
wenzelm [Fri, 26 Aug 2022 12:38:00 +0200] rev 75983
removed unused "def_theory" markup (stemming from be49c660ebbf), superseded e.g. by Document_Info.theory_by_file();
Fri, 26 Aug 2022 12:26:58 +0200 more aggressive clean_directory(session_dir), while rm_tree is guarded by check_directory, i.e. it is presumably "owned" by Browser_Info.build_session();
wenzelm [Fri, 26 Aug 2022 12:26:58 +0200] rev 75982
more aggressive clean_directory(session_dir), while rm_tree is guarded by check_directory, i.e. it is presumably "owned" by Browser_Info.build_session();
Fri, 26 Aug 2022 12:10:29 +0200 clarified signature;
wenzelm [Fri, 26 Aug 2022 12:10:29 +0200] rev 75981
clarified signature;
Fri, 26 Aug 2022 12:07:24 +0200 tuned signature;
wenzelm [Fri, 26 Aug 2022 12:07:24 +0200] rev 75980
tuned signature;
Fri, 26 Aug 2022 11:57:05 +0200 clarified signature;
wenzelm [Fri, 26 Aug 2022 11:57:05 +0200] rev 75979
clarified signature;
Fri, 26 Aug 2022 11:46:53 +0200 tuned whitespace;
wenzelm [Fri, 26 Aug 2022 11:46:53 +0200] rev 75978
tuned whitespace;
Fri, 26 Aug 2022 11:41:59 +0200 more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
wenzelm [Fri, 26 Aug 2022 11:41:59 +0200] rev 75977
more robust: ensure that chapter/session/theory do not contain special notation (like "/" or "..");
Fri, 26 Aug 2022 12:43:07 +0100 merged
paulson [Fri, 26 Aug 2022 12:43:07 +0100] rev 75976
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 tip