On 14/02/11 14:01, Lu Zhao wrote: > I have a situation like this that makes removing a defined term > desirable. I first define a function: > val FOO_def = Define `FOO bsp ksp = ...` > and later its parameter > val bsp_def = Define `bsp = ...` > I define bsp_def, because the right hand side of bsp definition is very > long for which I'd like to use a short name for it (in this case, it's > simply "bsp"), so I can easily see the function application.
You could call delete_const "bsp" This only works for constants in your current segment (which seems to be the case from your example). You could also do hide "bsp" which only affects the parser/pretty-printer. This has the advantage that you can later call reveal "bsp" to put the constant back into the parser/printer. But to be honest, I'd solve this problem by doing FOO_def = Define`FOO bsp ksp = ....` val BSP_def = Define`BSP = ...` so that the definition will always replay safely, and so too will the definition of BSP. If you stick to some convention (like uppercase letters only appear in constants, say), you should be able to avoid problems if you are frequently defining and redefining things. Michael ------------------------------------------------------------------------------ The ultimate all-in-one performance toolkit: Intel(R) Parallel Studio XE: Pinpoint memory and threading errors before they happen. Find and fix more than 250 security defects in the development cycle. Locate bottlenecks in serial and parallel code that limit performance. http://p.sf.net/sfu/intel-dev2devfeb _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
