tools.icl 7.69 KB
Newer Older
1 2 3 4
implementation module tools

import StdBool, StdFunc, StdFile, StdPStClass, StdSystem
import ExtNotice, StdPathname
John van Groningen's avatar
John van Groningen committed
5
import IdeState, UtilIO, UtilObjectIO, PmPath, projwin
6 7 8 9

//-- call out to supporting applications...

timepsuf	=: " Time Profile.pcl"
10
timeparg	=: " "
11 12

heappsuf	=: " Heap Profile0.hcl"
13
heapparg	=: " "
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75

proofsuf	=: ".prj"
proofarg	=: " "

shoprofun :: !*(PSt General) -> *PSt General
shoprofun ps
	# (prj,ps)		= getProject ps
	# execpath		= PR_GetExecPath prj
	// approximate name mangling done by RTE
	// should still take into account max filename length
	# profpath		= quoted_string (RemoveSuffix` execpath +++ timepsuf)
	# (prefs,ps)	= getPrefs ps

	# pcl_path				= prefs.reg_prefs.tp_path
	# (app_path,ps)			= accFiles GetFullApplicationPath ps
	# app_path				= GetLongPathName app_path
	# pcl_path				= fulAppPath app_path pcl_path
	# pcl_path				= case GetShortPathName pcl_path of
								(True,pcl_path)	-> pcl_path
								_				-> pcl_path

	# timepapp		= quoted_string (pcl_path +++ prefs.reg_prefs.tp_name)
	# sp			= timepapp +++ timeparg +++ profpath
	# stup			= RemoveFilename execpath
	# (ok,ps)		= accFiles (FExists stup) ps
	# stup			= if ok (stup +++ "\\") (applicationpath "")
	# (ok,ps)		= accFiles (LaunchApplication sp stup False) ps
	| not ok
		= openNotice (Notice ["Unable to launch " +++  sp +++ ".",stup] (NoticeButton "OK" id) []) ps
	= ps

shoheapfun :: !*(PSt General) -> *PSt General
shoheapfun ps
	# (prj,ps)		= getProject ps
	# execpath		= PR_GetExecPath prj
	// approximate name mangling done by RTE
	// should still take into account max filename length
	# profpath		= quoted_string (RemoveSuffix` execpath +++ heappsuf)
	# (prefs,ps)	= getPrefs ps

	# pcl_path				= prefs.reg_prefs.hp_path
	# (app_path,ps)			= accFiles GetFullApplicationPath ps
	# app_path				= GetLongPathName app_path
	# pcl_path				= fulAppPath app_path pcl_path
	# pcl_path				= case GetShortPathName pcl_path of
								(True,pcl_path)	-> pcl_path
								_				-> pcl_path

	# heappapp		= quoted_string (pcl_path +++ prefs.reg_prefs.hp_name)
	# sp			= heappapp +++  heapparg +++  profpath
	# stup			= RemoveFilename execpath
	# (ok,ps)		= accFiles (FExists stup) ps
	# stup			= if ok (stup +++ "\\") (applicationpath "")
	# (ok,ps)		= accFiles (LaunchApplication sp stup False) ps
	| not ok
		= openNotice (Notice ["Unable to launch " +++  sp +++ ".",stup] (NoticeButton "OK" id) []) ps
	= ps

provefun :: !*(PSt General) -> *PSt General
provefun ps
	# ps			= pm_save ps	// ensure project file is recent...
	
76
	# (pathname,ps) = getProjectFilePath ps
77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
	# pr_path		= quoted_string (RemoveSuffix` pathname +++. proofsuf)
	# (prefs,ps)	= getPrefs ps

	# pcl_path				= prefs.reg_prefs.pr_path
	# (app_path,ps)			= accFiles GetFullApplicationPath ps
	# app_path				= GetLongPathName app_path
	# pcl_path				= fulAppPath app_path pcl_path
	# pcl_path				= case GetShortPathName pcl_path of
								(True,pcl_path)	-> pcl_path
								_				-> pcl_path

	# proofapp		= quoted_string (pcl_path +++ prefs.reg_prefs.pr_name)
	# cps			= proofapp +++ proofarg +++ pr_path
	# stup			= RemoveFilename pathname
	# (ok,ps)		= accFiles (FExists stup) ps
	# stup			= if ok (stup +++ "\\") (applicationpath "")
	# (ok,ps)		= accFiles (LaunchApplication cps stup False) ps
	| not ok
		= openNotice (Notice ["Unable to launch " +++  cps +++ "."] (NoticeButton "OK" id) []) ps
	= ps

98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
:: ToolInfo =
	{ tpId			:: !Id
	, tpString		:: !String
	, hpId			:: !Id
	, hpString		:: !String
	, prId			:: !Id
	, prString		:: !String
	}

toolData :: !.Prefs !*(PSt General) -> *(!.ToolInfo,!*PSt General)
toolData prefs ps
	# (tpId,ps)		= openId ps
	# (hpId,ps)		= openId ps
	# (prId,ps)		= openId ps
	# iniTPString	= prefs.reg_prefs.tp_path +++ prefs.reg_prefs.tp_name
	# iniHPString	= prefs.reg_prefs.hp_path +++ prefs.reg_prefs.hp_name
	# iniPRString	= prefs.reg_prefs.pr_path +++ prefs.reg_prefs.pr_name
	# ti			=
						{ tpId			= tpId
						, tpString		= iniTPString
						, hpId			= hpId
						, hpString		= iniHPString
						, prId			= prId
						, prString		= iniPRString
						}
	= (ti,ps)


toolOptions :: !.ToolInfo -> (:+: .TextControl (:+: .EditControl (:+: .ButtonControl (:+: .TextControl (:+: .EditControl (:+: .ButtonControl (:+: .TextControl (:+: .EditControl (:+: .ButtonControl .ButtonControl)))))))) .a *(PSt *General))
toolOptions ti=:{tpId,tpString,hpId,hpString,prId,prString} 
	=	TextControl "Time Profiler:" [ControlPos (Left,zero),ControlWidth (ContentWidth "Theorem Prover:")]
	:+: EditControl tpString (PixelWidth 300) 1 [ControlId tpId,ControlSelectState Unable]
	:+: ButtonControl "Select..." [ControlFunction (noLS (setTP tpId))]
	:+: TextControl "Heap Profiler:" [ControlPos (Left,zero),ControlWidth (ContentWidth "Theorem Prover:")]
	:+: EditControl hpString (PixelWidth 300) 1 [ControlId hpId,ControlSelectState Unable]
	:+: ButtonControl "Select..." [ControlFunction (noLS (setHP hpId))]
	:+: TextControl "Theorem Prover:" [ControlPos (Left,zero),ControlWidth (ContentWidth "Theorem Prover:")]
	:+: EditControl prString (PixelWidth 300) 1 [ControlId prId,ControlSelectState Unable]
	:+: ButtonControl "Select..." [ControlFunction (noLS (setPR prId))]
	:+: ButtonControl "Clear Registry" [ControlPos (Left,zero),ControlFunction (noLS clearRegistry)]


//import dodebug
import first_run, PmPath, StdList

setTP tpId ps
	# (prefs,ps)	= getPrefs ps
	# (result,ps)	= selectOutputFile` "Select time profiler" "*.exe" "Set" ps
	| isNothing result = ps
	# full			= fromJust result
	# name			= GetFileName full
	# short			= case GetShortPathName full of
						(True,short)	-> short
						_				-> full
	# rpath			= GetFilePath short
	# (app_path,ps)	= getStup ps
	# spath			= symAppPath app_path (GetFilePath full)
	# ps			= appPIO (setControlText tpId (spath +++ name)) ps
	# prefs			= {prefs & reg_prefs.tp_name = name, reg_prefs.tp_path = spath}
	# ps			= setPrefs prefs ps
158
	# (ide_name,ide_path,errs)
159
					= get_ide_from_registry
160
	| not (isEmpty errs) || ide_name == "" || ide_path == "" = ps
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
	# errs			= change_pcl_registry_fun ide_name ide_path name rpath
	| errs == []	= ps
	= ps

setHP hpId ps
	# (prefs,ps)	= getPrefs ps
	# (result,ps)	= selectOutputFile` "Select heap profiler" "*.exe" "Set" ps
	| isNothing result = ps
	# full			= fromJust result
	# name			= GetFileName full
	# short			= case GetShortPathName full of
						(True,short)	-> short
						_				-> full
	# rpath			= GetFilePath short
	# (app_path,ps)	= getStup ps
	# spath			= symAppPath app_path (GetFilePath full)
	# ps			= appPIO (setControlText hpId (spath +++ name)) ps
	# prefs			= {prefs & reg_prefs.hp_name = name, reg_prefs.hp_path = spath}
	# ps			= setPrefs prefs ps
180
	# (ide_name,ide_path,errs)
181
					= get_ide_from_registry
182
	| not (isEmpty errs) || ide_name == "" || ide_path == "" = ps
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
	# errs			= change_hcl_registry_fun ide_name ide_path name rpath
	| errs == []	= ps
	= ps

setPR prId ps
	# (prefs,ps)	= getPrefs ps
	# (result,ps)	= selectOutputFile` "Select theorem prover" "*.exe" "Set" ps
	| isNothing result = ps
	# full			= fromJust result
	# name			= GetFileName full
	# short			= case GetShortPathName full of
						(True,short)	-> short
						_				-> full
	# rpath			= GetFilePath short
	# (app_path,ps)	= getStup ps
	# spath			= symAppPath app_path (GetFilePath full)
	# ps			= appPIO (setControlText prId (spath +++ name)) ps
	# prefs			= {prefs & reg_prefs.pr_name = name, reg_prefs.pr_path = spath}
	= setPrefs prefs ps

clearRegistry ps
	# (errs,ps)		= uninstall ps
	| errs == [] = ps
	# (okId,ps)		= openId ps
	# (dlogId,ps)	= openId ps
	# (_,ps)		= openModalDialog Void (Dialog "Clear Registry errors"
						(	TextControl "Clear Registry produced an error:"	[]
						:+:	TextControl (hd errs) [ControlPos (Left,zero)]
						:+: ButtonControl "OK" [ControlId okId,ControlFunction (noLS (closeWindow dlogId))]) 
						[WindowOk okId,WindowId dlogId]) ps
	= ps