| 65 |
handle Option => raise Fail "bn2statenv" |
handle Option => raise Fail "bn2statenv" |
| 66 |
|
|
| 67 |
(* exec_group is basically the same as ET.group with |
(* exec_group is basically the same as ET.group with |
| 68 |
* two additional actions to be taken: |
* one additional actions to be taken: |
| 69 |
* 1. Before executing the code, we announce the priviliges |
* Before executing the code, we announce the priviliges |
| 70 |
* that are being invoked. (For the time being, we assume |
* that are being invoked. (For the time being, we assume |
| 71 |
* that everybody has every conceivable privilege, but at the |
* that everybody has every conceivable privilege, but at the |
| 72 |
* very least we announce which ones are being made use of.) |
* very least we announce which ones are being made use of.) *) |
|
* 2. After we are done we must make the values of "shared" |
|
|
* compilation units permanent. *) |
|
| 73 |
fun exec_group gp (g as GroupGraph.GROUP { required = rq, ... }) = |
fun exec_group gp (g as GroupGraph.GROUP { required = rq, ... }) = |
| 74 |
(if StringSet.isEmpty rq then () |
(if StringSet.isEmpty rq then () |
| 75 |
else Say.say ("$Execute: required privileges are:\n" :: |
else Say.say ("$Execute: required privileges are:\n" :: |
Parent Directory
| 
Revision Log
| 
Patch
