public class MacroManager
extends java.lang.Object
Even though WorkVar and related classes are defined in the mmj.lang package, WorkVarBoss is coded as a separate "boss" so that Work Vars can be treated as a separate set of resources, separate from Logical System, Proof Assistant, etc. Initially though, WorkVars and friends are to be used with Proof Assistant -- and nowhere else.
Modifier and Type | Class and Description |
---|---|
static class |
MacroManager.CallbackType |
static class |
MacroManager.ExecutionMode |
Modifier and Type | Field and Description |
---|---|
Setting<java.lang.String> |
macroExtension |
Setting<java.io.File> |
macroFolder |
Setting<java.lang.String> |
macroLanguage |
Setting<java.io.File> |
prepMacro |
Constructor and Description |
---|
MacroManager(SessionStore store,
java.util.function.Supplier<ProofAsst> proofAsst)
Constructor from settings storage and message output.
|
Modifier and Type | Method and Description |
---|---|
java.lang.Object |
evalRaw(java.lang.String code)
Execute a piece of script code.
|
java.lang.Object |
get(java.lang.String key)
Get a named variable's value.
|
javax.script.ScriptEngine |
getEngine() |
javax.script.ScriptEngine |
getEngine(java.lang.String initMacro) |
void |
runCallback(MacroManager.CallbackType c)
Run a macro callback.
|
void |
runMacro(MacroManager.ExecutionMode mode,
java.lang.String[] args)
Run a macro given an argument list.
|
void |
runMacro(MacroStmt macroStmt)
Run a macro given a macro statement.
|
void |
runMacroRaw(java.lang.String name)
Run a macro with the given name.
|
void |
set(java.lang.String key,
java.lang.Object value)
Set a named variable's value.
|
void |
setCallback(MacroManager.CallbackType c,
java.lang.Runnable r)
Sets the callback for a given type of event.
|
boolean |
setPrepMacro(java.lang.String prep)
Set the preparation macro.
|
public Setting<java.io.File> macroFolder
public Setting<java.lang.String> macroLanguage
public Setting<java.lang.String> macroExtension
public Setting<java.io.File> prepMacro
public MacroManager(SessionStore store, java.util.function.Supplier<ProofAsst> proofAsst)
store
- settings storageproofAsst
- A callback to get the ProofAsst object when neededpublic java.lang.Object get(java.lang.String key)
key
- the variable namepublic void set(java.lang.String key, java.lang.Object value)
key
- the variable namevalue
- The variable valuepublic boolean setPrepMacro(java.lang.String prep)
prepMacro
.setString(prep)
.prep
- The macro name relative to the macro directory (
macroFolder
).public void runMacro(MacroManager.ExecutionMode mode, java.lang.String[] args) throws java.lang.IllegalArgumentException
mode
- The method in which this macro is getting called (for
distinguishing which variables are set)args
- The argument list; args[0]
is the macro name.java.lang.IllegalArgumentException
- if there are any errorspublic void setCallback(MacroManager.CallbackType c, java.lang.Runnable r)
c
- The type of callback (event trigger)r
- An interface to override with a (javascript) functionpublic void runCallback(MacroManager.CallbackType c)
c
- The type of callback (event trigger)public void runMacro(MacroStmt macroStmt) throws java.lang.IllegalArgumentException
macroStmt
- The macro statement (from e.g. a proof worksheet)java.lang.IllegalArgumentException
- if there are any errorspublic void runMacroRaw(java.lang.String name) throws java.lang.IllegalArgumentException
name
- Name of the macro, looked up in macros/ folderjava.lang.IllegalArgumentException
- if an error occurredpublic java.lang.Object evalRaw(java.lang.String code) throws javax.script.ScriptException
code
- A string of code to execute.javax.script.ScriptException
- if an error occurredpublic javax.script.ScriptEngine getEngine()
public javax.script.ScriptEngine getEngine(java.lang.String initMacro)