1 files changed, 34 insertions, 0 deletions
diff --git a/app/flint/0.4/src/operator.manager b/app/flint/0.4/src/operator.manager
new file mode 100644
index 0000000..fc9c31a
--- /dev/null
+++ b/app/flint/0.4/src/operator.manager
@@ -0,0 +1,34 @@
+PACKET operator manager                          (* Autor: Thomas Berlage *)
+                                                 (* Stand: 14.01.88       *)
+  DEFINES
+
+  operator manager,
+  continue :
+
+
+LET
+  only privileged =
+    "Nur für Systemtasks zugelassen";
+
+
+PROC operator manager (DATASPACE VAR ds, INT CONST order, phase,
+                       TASK CONST order task) :
+
+  enable stop;
+  IF order task = supervisor OR order task < supervisor THEN
+    menue manager (ds, order, phase, order task)
+  ELSE
+    errorstop (only privileged)
+  END IF
+
+END PROC operator manager;
+
+PROC continue (TASK CONST t) :
+
+  continue (t,
+    PROC (DATASPACE VAR, INT CONST, INT CONST, TASK CONST) operator manager)
+
+END PROC continue;
+
+END PACKET operator manager;
+