Theorema Downloader

Version 1.0, 2017-03-29
Alexander Maletzky ⟨alexander.maletzky@risc.jku.at⟩, RISC, JKU Linz

Step 1: Set the installation directory of Theorema.

Set the global variable $TheoremaDir to the path of your Theorema installation directory (the one containing file “Common.m” and sub-directories “Language”, “Interface”, ...). Function getValidTmaDir[] can be used to find the right directory.

$TheoremaDir=getValidTmaDir[]

Step 2: List all available packages.

Command listAvailablePackages[] lists all available packages. It does not provide information about which of the packages you have installed already.

listAvailablePackages[]

Step 3: Download and install the package of your choice.

Execute command installPackage, with the name of the package you want to download and install as parameter (the name is a string!).

Attention! Existing files are overwritten. This normally does not affect files that are part of the standard distribution of Theorema, but it may well affect files stemming from other packages and/or previous versions of the new package that have been installed before.

installPackage[""]

Implementation

$baseURL = "http://www.risc.jku.at/projects/tetra-gb/AddOns/";

ClearAll[ installPackage];
installPackage[ name_String] :=
	If[ StringQ[ $TheoremaDir],
		installPackage[ name, $TheoremaDir],
	(*else*)
		Replace[ getValidTmaDir[],
			{
				dir_String :> (Print[ "Installing package in " <> dir <> "."]; installPackage[ name, dir]),
				_ -> "ERROR: Theorema installation directory not found."
			}
		]
	]
installPackage[ name_String, tmaDir_String] :=
	With[ {ext = ".zip"},
	With[ {dir = $TemporaryDirectory,
			url = $baseURL <> StringReplace[ name, " " -> "%20"] <> ext},
	With[ {newDir = FileNameJoin[ {dir, name}]},
	Module[ {progress = 0., task = "Downloading package ..."},
	Module[ {progFunction, code = Null},
		progFunction[ _, "progress", {dlnow_, dltotal_, _, _}] := Quiet[ progress = dlnow / (2. * dltotal)];
		progFunction[ _, "error", _] :=
			Quiet[
				progress = 1.;
				task = "ERROR: An error occurred while downloading the package. Check your internet connection."
			];
		progFunction[ _, "statuscode", c_] := Quiet[ code = c];
		progFunction[ _, "data", _] :=
			If[ MemberQ[ code, 404],
				DeleteFile[ newDir <> ext];
				progress = 1.;
				task = "ERROR: Package not found.",
			(*else*)
				progress = 0.66;
				task = "Extracting archive ...";
				If[ FileExistsQ[ newDir], DeleteDirectory[ newDir, DeleteContents -> True]];
				ExtractArchive[ newDir <> ext, dir];
				progress = 0.83;
				task = "Copying files ...";
				With[ {readme = copyPackageFiles[ newDir, tmaDir, True]},
					progress = 0.95;
					task = "Cleaning-up ...";
					DeleteDirectory[ newDir, DeleteContents -> True];
					DeleteFile[ newDir <> ext];
					progress = 1.;
					task = "Done";
					If[ StringQ[ readme],
						CreateDocument[ TextCell[ readme], WindowTitle -> name <> " — README.txt"]
					];
				];
			];
		URLSaveAsynchronous[ url, newDir <> ext, progFunction, "Progress" -> True];
		Row[ {ProgressIndicator[ Dynamic[ progress]], Dynamic[ task]}, Spacer[ 5]]
	]]]]]

ClearAll[ listAvailablePackages];
listAvailablePackages[] :=
	With[ {dir = $TemporaryDirectory,
			url = $baseURL <> "list.txt"},
	With[ {file = FileNameJoin[ {dir, "TmaAddOns.txt"}]},
	Module[ {res = "Searching ..."},
	Module[ {progFunction, code = Null},
		progFunction[ _, "error", _] :=
			(res = "ERROR: An error occurred while searching the list of packages. Check your internet connection.");
		progFunction[ _, "statuscode", c_] := Quiet[ code = c];
		progFunction[ _, "data", _] :=
			(
				If[ MemberQ[ code, 404],
					res = "ERROR: List not found.",
				(*else*)
					res = displayPackages[ listAvailablePackages[ file]]
				];
				DeleteFile[ file]
			);
		URLSaveAsynchronous[ url, file, progFunction];
		Dynamic[ res]
	]]]]
listAvailablePackages[ file_String] :=
	With[ {packages = StringSplit[ ReadString[ file], "\n"]},
		Map[
			Function[ p,
				Replace[ StringSplit[ p, "::"],
					Except[ _List] -> Sequence[]
				]
			],
			packages
		]
	]

ClearAll[ displayPackages];
displayPackages[ {header_List, rest___List}] :=
	TableForm[ {rest}, TableHeadings -> {None, header}]

ClearAll[ getValidTmaDir];
getValidTmaDir[] :=
	Replace[ Cases[ $Path, d_String :> With[ {res = getValidTmaDir[ d]}, res /; StringQ[ res]], {1}, 1],
		{
			{dir_String} :> dir,
			_ -> $Failed
		}
	]
getValidTmaDir[ dir_String] :=
	Which[
		FileExistsQ[ FileNameJoin[ {dir, "Common.m"}]],
		dir,
	(*else*)
		FileExistsQ[ FileNameJoin[ {dir, "Theorema"}]],
		FileNameJoin[ {dir, "Theorema"}],
	(*else*)
		True,
		$Failed
	]

ClearAll[ copyPackageFiles];
copyPackageFiles[ src_String, tar_String, top_] :=
	With[ {contents = FileNames[ All, src]},
	With[ {dirPos = Position[ contents, _String?(DirectoryQ[ #]&), {1}]},
	With[ {files = Delete[ contents, dirPos], dirs = Extract[ contents, dirPos]},
	Module[ {res = Null},
		If[ TrueQ[ top],
			Scan[
				If[ FileNameTake[ #] === "README.txt",
					res = ReadString[ #],
				(*else*)
					CopyFile[ #, FileNameJoin[ {tar, FileNameTake[ #]}], OverwriteTarget -> True]
				]&,
				files
			],
		(*else*)
			Scan[ CopyFile[ #, FileNameJoin[ {tar, FileNameTake[ #]}], OverwriteTarget -> True]&, files]
		];
		Scan[
			With[ {base = FileNameTake[ #]},
			With[ {new = FileNameJoin[ {tar, base}]},
				If[ FileExistsQ[ new],
					copyPackageFiles[ #, new, False],
				(*else*)
					CopyDirectory[ #, new]
				]
			]]&,
			dirs
		];
		res
	]]]]