isabelle: src/Pure/System/cygwin.scala@0a43fc778cd2 (annotated)

31499 4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	1	/* Title: Pure/System/cygwin.scala
45673 cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library; wenzelm parents: 45667 diff changeset	2	Module: PIDE
31499 4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	3	Author: Makarius
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	4
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	5	Accessing the Cygwin installation.
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	6	*/
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	7
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	8	package isabelle
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	9
43520 cec9b95fa35d explicit import java.lang.System to prevent odd scope problems; wenzelm parents: 41333 diff changeset	10	import java.lang.System
31826 7f311da87d5a some more Cygwin checks; wenzelm parents: 31499 diff changeset	11	import java.io.File
34219 d37cfca69887 Standard_System.raw_execute: optional cwd; wenzelm parents: 34203 diff changeset	12	import java.net.URL
d37cfca69887 Standard_System.raw_execute: optional cwd; wenzelm parents: 34203 diff changeset	13	import java.awt.Component
31499 4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	14
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	15
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	16	object Cygwin
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	17	{
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	18	/* Cygwin installation */
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	19
34220 f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	20	private def sanity_check(root: File)
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	21	{
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	22	if (!new File(root, "bin\\bash.exe").isFile \|\|
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	23	!new File(root, "bin\\env.exe").isFile \|\|
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	24	!new File(root, "bin\\tar.exe").isFile)
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	25	error("Bad Cygwin installation: " + root.toString)
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	26	}
f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	27
34045 bc71778a327d simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway); wenzelm parents: 34043 diff changeset	28	def check_root(): String =
31826 7f311da87d5a some more Cygwin checks; wenzelm parents: 31499 diff changeset	29	{
47996 25b9f59ab1b9 simplified Cygwin root: warm start via env, cold start via property, no registry magic; wenzelm parents: 47679 diff changeset	30	val cygwin_root1 = System.getenv("CYGWIN_ROOT")
25b9f59ab1b9 simplified Cygwin root: warm start via env, cold start via property, no registry magic; wenzelm parents: 47679 diff changeset	31	val cygwin_root2 = System.getProperty("cygwin.root")
34045 bc71778a327d simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway); wenzelm parents: 34043 diff changeset	32	val root =
47996 25b9f59ab1b9 simplified Cygwin root: warm start via env, cold start via property, no registry magic; wenzelm parents: 47679 diff changeset	33	if (cygwin_root1 != null && cygwin_root1 != "") cygwin_root1
25b9f59ab1b9 simplified Cygwin root: warm start via env, cold start via property, no registry magic; wenzelm parents: 47679 diff changeset	34	else if (cygwin_root2 != null && cygwin_root2 != "") cygwin_root2
25b9f59ab1b9 simplified Cygwin root: warm start via env, cold start via property, no registry magic; wenzelm parents: 47679 diff changeset	35	else error("Bad Cygwin installation: unknown root")
34220 f7a0088518e1 tuned error handling; wenzelm parents: 34219 diff changeset	36	sanity_check(new File(root))
34045 bc71778a327d simplified Cygwin setup, assuming 1.7 registry layout (version 1.5 suffers from upcaseenv problem anyway); wenzelm parents: 34043 diff changeset	37	root
31826 7f311da87d5a some more Cygwin checks; wenzelm parents: 31499 diff changeset	38	}
31499 4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	39	}
4345173ee386 Accessing the Cygwin installation. wenzelm parents: diff changeset	40

author	wenzelm
	Thu, 24 May 2012 23:28:58 +0200
changeset 47997	0a43fc778cd2
parent 47996	25b9f59ab1b9
permissions	-rw-r--r--