diff --git a/cafeobj/command-top.lisp b/cafeobj/command-top.lisp
index 305bc6f..6574558 100644
--- a/cafeobj/command-top.lisp
+++ b/cafeobj/command-top.lisp
@@ -274,6 +274,7 @@
 ;;; 
 (defparameter .?-invalid-chars. '("." "#" "'" "`"))
 
+#||
 (defun cafeobj-what-is (inp)
   (flet ((check-pat (pat)
            (if (not (some #'(lambda (str)
@@ -298,6 +299,25 @@
       (if desc
           (format t desc)
         (format t "~&Unknown command/switch or message ID: ~{~a ~^~}." (cdr inp))))))
+||#
+
+(defun cafeobj-what-is (inp)
+  (let* ((ask (intern (car inp)))
+	 (question (cdr inp))
+	 (key (reduce #'(lambda (x y) (concatenate 'string x y)) question))
+	 (description nil))
+    (case ask
+      (|?| (setq description (get-document-string key)))
+      ;; (|??| (setq description (get-detailed-document key)))
+      ;; ((|?ex| |?example|) (setq description (get-example key)))
+      (otherwise
+       ;; this cannot happen
+       (with-output-chaos-error ('internal-error)
+	 (format t "Unknown help command ~a" (car inp)))))
+    (cond (description
+	   (format t (format-description description)))
+	  (t	(with-output-chaos-warning ()
+		  (format t "System does not know about \"~{~a~^~}\"." question))))))
 
 ;;; 
 (defun get-command-description (level id)
@@ -460,80 +480,6 @@
   #+CLISP (ext::exit))
 
 ;;;
-;;; DEFCOM
-;;;
-(defvar *cafeobj-commands* (make-hash-table :test #'equal))
-
-(defstruct (command (:print-function print-command))
-  (name "" :type string)		; command name
-  (category nil :type symbol)		; command types
-  (parser nil :type symbol)		; parser function
-  (evaluator nil :type symbol)		; evaluator function
-  (help-string "" :type string))	; command's help string
-
-(defun print-command (me &optional (stream *standard-output*) &rest ignore)
-  (declare (ignore ignore))
-  (format stream "~&** command     : ~a" (command-name me))
-  (format stream "~%   category    : ~a" (command-category me))
-  (format stream "~%   parser      : ~a" (command-parser me))
-  (format stream "~%   evaluator   : ~a" (command-evaluator me))
-  (format stream "~%   description : ~a" (command-help-string me)))
-
-(defun print-command-usage (command &optional (stream *standard-output*))
-  (let ((com (if (command-p command)
-		 command
-	       (and (stringp command)
-		    (gethash command *cafeobj-commands*)))))
-    (unless com
-      (with-output-chaos-error ('no-com)
-	(format t "No such command '~a'" command)))
-    (format stream "~&~a : ~a" (command-name com) (command-help-string com))))
-
-(defmacro defcom ((&rest names) doc-string category parser evaluator)
-    (unless (fboundp parser) (warn "no parser ~s" parser))
-    (unless (fboundp evaluator) (warn "no evaluator ~s" evaluator))
-  `(dolist (name ',names)
-    (setf (gethash name *cafeobj-commands*)
-      (make-command :name name
-		    :category ',category
-		    :parser ',parser
-		    :evaluator ',evaluator
-		    :help-string ,doc-string))))
-;;;
-;;; DEFDECL
-;;;
-(defstruct (decl (:print-function print-decl) (:include command)))
-
-(defmacro defdecl ((&rest names) doc-string category parser evaluator)
-    (unless (fboundp parser) (warn "no parser ~s" parser))
-    (unless (fboundp evaluator) (warn "no evaluator ~s" evaluator))
-  `(dolist (name ',names)
-    (setf (gethash name *cafeobj-declarations*)
-      (make-decl :name name
-		 :category ',category
-		 :parser ',parser
-		 :evaluator ',evaluator
-		 :help-string ,doc-string))))
-
-(defun print-decl (me &optional (stream *standard-output*) &rest ignore)
-  (declare (ignore ignore))
-  (format stream "~&** declaration : ~a" (decl-name me))
-  (format stream "~%   category    : ~a" (decl-category me))
-  (format stream "~%   parser      : ~a" (decl-parser me))
-  (format stream "~%   evaluator   : ~a" (decl-evaluator me))
-  (format stream "~%   description : ~a" (decl-help-string me)))
-
-(defun print-decl-usage (decl &optional (stream *standard-output*))
-  (let ((decl (if (decl-p decl)
-		 decl
-	       (and (stringp decl)
-		    (gethash decl *cafeobj-declarations*)))))
-    (unless decl
-      (with-output-chaos-error ('no-decl)
-	(format t "No such declaration form '~a'" decl)))
-    (format stream "~&~a : ~a" (decl-name decl) (decl-help-string decl))))
-
-;;;
 ;;; NOP
 ;;;
 (defun cafeobj-nop (&rest ignore)
@@ -544,11 +490,11 @@
 ;;;
 (defun cafeobj-evaluate-command (key inp)
   (declare (type string key))
-  (let ((com (gethash key *cafeobj-commands*)))
+  (let ((com (get-command-info key)))
     (unless com
       (with-output-chaos-error ('no-commands)
 	(format t "No such command or declaration keyword '~a'." key)))
-    (let ((parser (command-parser com)))
+    (let ((parser (comde-parser com)))
       (unless parser
 	(with-output-chaos-error ('no-parser)
 	  (format t "No parser is defined for command ~a" key)))
@@ -557,8 +503,8 @@
 	  (with-output-chaos-error ('parse-error)
 	    (format t "Invalid argument to command ~a." key)))
 	(if (eq pform :help)
-	    (print-command-usage com)
-	  (let ((evaluator (command-evaluator com)))
+	    (print-comde-usage com)
+	  (let ((evaluator (comde-evaluator com)))
 	    (unless evaluator
 	      (with-output-chaos-error ('no-evaluator)
 		(format t "No evaluator is defined for command ~a." key)))
diff --git a/cafeobj/commands.lisp b/cafeobj/commands.lisp
new file mode 100644
index 0000000..0d2a600
--- /dev/null
+++ b/cafeobj/commands.lisp
@@ -0,0 +1,962 @@
+;;;-*- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp -*-
+#|==============================================================================
+                            System: CHAOS
+                           Module: cafeobj
+                         File: commands.lisp
+==============================================================================|#
+(in-package :chaos)
+#-:chaos-debug
+(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
+#+:chaos-debug
+(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
+
+(eval-when (:execute :load-toplevel)
+
+;;; ---------------------------------------------------------------------------
+;;; these hash tables are used for register keywords, document strings.
+;;; these are used by toplevel command interpreter
+;;; and cafeobj language construct evaluators.
+;;; ---------------------------------------------------------------------------
+
+  ;; halds systems toplevel commands, declarations accepted by top level
+  (clrhash *cafeobj-top-commands*)
+
+  ;; holds all of the declaration forms
+  (clrhash *cafeobj-declarations*)
+
+  ;; this holds each commands/language constructs document strings.
+  ;; systems' doc-generator refers to this hash table.
+ (clrhash *cafeobj-doc-db*)
+
+;;; --------------------------------------------------------------------------
+;;; all of the declarations/commands in alphabetical order.
+;;; --------------------------------------------------------------------------
+  
+(define ("??" "?")
+    :category :help
+    :parser identity
+    :evaluator cafeobj-top-level-help
+        :doc "
+## `?` ## {#help}
+
+lists all top-level commands. The `?` can be used after many of the
+top-level commands to obtain help.
+")
+
+
+(define ("!")
+    :category :misc
+    :parser parse-shell-command
+    :evaluator eval-ast
+        :doc "
+## `! <command>` ## {#commandexec}
+
+TODO Currently not working!! 
+
+On Unix only, forks a shell and executes the given `<command>`.
+")
+
+
+(define ("--" "**")
+    :category :decl-toplevel
+    :parser parse-comment-command
+    :evaluator identity
+    :doc "
+")
+
+
+(define ("-->" "**>")
+    :doc "
+"
+    :category :decl-toplevel
+    :parser parse-comment-command
+    :evaluator eval-ast)
+
+(define ("=")
+    :type :doc-only
+    :doc "
+## `=` ## {#axeq}
+
+The syntax element `=` introduces an axiom of the equational theory,
+and is different from `==` which specifies an equality based on
+rewriting. 
+
+Related: [`==`](#equality) [`eq`](#eq)
+")
+
+(define ("==")
+    :type :doc-only
+    :doc "
+## `==` ## {#equality}
+
+The predicate `==` is a binary operator defined for each visible sort
+and is defined in terms of evaluation. That is, for ground terms `t`
+and `t'` of the same sort, `t == t'` evaluates to `true` iff terms
+reduce to a common term. This is different from the equational `=`
+which specifies the equality of the theory.
+")
+
+(define ("=>")
+    :type :doc-only
+    :doc
+    "
+## `==>` ## {#transrel}
+
+This binary predicate is defined on each visible sort, and defines the
+transition relation, which is reflexive, transitive, and closed under
+operator application. It expresses the fact that two states (terms)
+are connected via transitions.
+Related: [`trans`](#trans) [`=(*)=>`](#transsearch)
+")
+
+(define ("=*=")
+    :type :doc-only
+    :doc "
+## `=*=` ## {#bequality}
+
+The predicate for behavioural equivalence, written `=*=`, is a binary
+operator defined on each hidden sort. 
+
+TODO: old manual very unclear ... both about `=*=` and 
+`accept =*= proof` ??? (page 46 of old manual)
+")
+
+(define  ("dribble")
+    :category :misc
+    :parser parse-dribble-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("mod" "module" "module*" "mod*" "module!" "mod!" "sys:mod!" "sys:module!" "sys:mod*" "sys:module*")
+    :category :decl-toplevel
+    :parser process-module-declaration-form
+    :evaluator eval-ast
+    :doc "
+## `module[!|*] <modname> [ ( <params> ) ] [ <principal_sort_spec> ] { mod_elements ... }` ## {#module}
+
+Alias: `mod`
+
+defines a module, the basic building block of \_cafeobj. Possible elements
+are declarations of 
+
+  - import - see `protecting`, `extending`, `including`, `using`
+  - sorts - see `sort declaration`
+  - variable - see `var`
+  - equation - see `op`, `eq`, `ceq`, `bop`, `beq`, `bceq`
+  - transition - see `trans`, `ctrans`, `btrans`, `bctrans`
+  
+`modname` is an arbitrary string.
+
+`module*` introduces a loose semantic based module.
+
+`module!` introduces a strict semantic based module.
+
+`module` introduces a module without specified semantic type.
+
+If `params` are given, it is a parametrized module. See `parametrized module`
+for more details.
+
+If `principal_sort_spec` is given, it has to be of the form
+`principal-sort <sortname>` (or `p-sort <sortname>`). The principal
+sort of the module is specified, which allows more concise `view`s from
+single-sort modules as the sort mapping needs not be given.
+")
+
+(define ("view")
+    :category :decl-toplevel
+    :parser process-view-declaration-form
+    :evaluator eval-ast
+    :doc "
+## `view <name> from <modname> to <modname> { <viewelems> }` ## {#view}
+
+A view specifies ways to bind actual parameters to formal parameters
+(see [parametrized module](#parametrizedmodule)). The view has to
+specify the mapping of the sorts as well as the operators. 
+
+The `<viewelems>` is a comma-separated list of expressions specifying
+these mappings:
+
+~~~~
+sort <sortname> -> <sortname>
+hsort <sortname> -> <sortname>
+op <opname> -> <opname>
+bop <opname> -> <opname>
+~~~~
+
+and also can contain variable declarations. 
+
+Infix operators are represented as terms containing the operator with
+either literal underscores `_`, or variables: `_*_` or `X * Y`.
+The `<opname>` can be qualified.
+
+Example: Assume a module `MONOID` with sort `M` and ops `e` and `*`
+are given, and another `SIMPLE-NAT` with sort `Nat` and operators `0`
+and `+` (with the same arity). Then the following expression
+constitutes a view:
+
+~~~~~
+view NAT-AS-MONOID from MONOID to SIMPLE-NAT {
+  sort M -> Nat,
+  op   e -> 0,
+  op _*_ -> _+_
+}
+~~~~~
+
+In specifying views some rules can be omitted:
+
+1. If the source and target modules have common submodules, all the
+  sorts and modules decalred therein are assumed to be mapped to
+  themselves;
+
+2. If the source and target modules have sorts and/or operators with
+  identical names, they are mapped to their respective counterparts;
+
+3. If the source module has a single sort and the target has a 
+  principal sort, the single sort is mapped to the principal sort.
+")
+
+(define ("check")
+    :category :checker
+    :parser   parse-check-command
+    :evaluator eval-ast
+    :doc "
+## `check <options>` ## {#check}
+
+This command allows for checking of certain properties of modules and
+operators. 
+
+`check regularity <mod_exp>`
+  ~ Checks whether the module given by the module expression
+    `<mod_exp>` is regular. 
+
+`check compatibility <mod_exp>`
+  ~ Checks whether term rewriting system of the module given by the
+    module expression `<mod_exp>` is compatible, i.e., every
+    application of every rewrite rule to every well-formed term
+    results in a well-formed term. (This is not necessarily the case
+    in order-sorted rewriting!)
+
+`check laziness <op_name>`
+  ~ Checks whether the given operator can be evaluated lazily. If not
+    `<op_name>` is given, all operators of the current module are
+    checked. 
+
+Related: [`regularize`](#regularize)
+")
+
+(define ("regularize")
+    :category :module
+    :parser parse-regularize-command
+    :evaluator eval-ast
+    :doc "
+## `regularize <mod-name>` ## {#regularize}
+
+Regularizes the signature of the given module, ensuring that every
+term has exactely one minimal parse tree. In this process additional
+sorts are generated to ensure unique least sort of all terms.
+
+Modules can be automatically regularized by the interpreter if the
+`regularize signature` switch is turn to `on`.
+
+TODO -- should we give more details here -- unclear to me.
+")
+
+(define ("exec" "execute")
+    :category :rewrite
+    :parser parse-exec-command
+    :evaluator eval-ast
+    :doc "
+## `execute [ in <mod-exp> : ] <term> .` ## {#execute}
+
+Alias: `exec`
+
+Reduce the given term in the given module, if `<mod-exp>` is given, 
+otherwise in the current module. 
+
+For `execute` equations and transitions, possibly conditional, are taken
+into account for reduction.
+
+Related: [`breduce`](#breduce) [`reduce`](#reduce)
+")
+
+(define ("red" "reduce")
+  :category :rewrite
+  :parser parse-reduce-command
+  :evaluator eval-ast
+  :doc "
+reduce [in <Modexpr> :] <Term> . ~%Rewrite <Term> by axioms of the module.
+")
+
+(define ("exec!" "execute!")
+    :category :rewrite
+    :parser parse-exec+-command
+    :evaluator eval-ast
+    :doc "
+exec! [in <Modexpr> :] <Term> .
+")
+
+(define ("bred" "breduce")
+    :category :rewrite
+    :parser parse-bred-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("version")
+    :category :misc
+    :parser parse-version-command
+    :evaluator princ
+    :doc "
+prints version number of the system.
+")
+
+(define ("cbred")
+    :category :rewrite
+    :parser parse-cbred-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("stop")
+    :category :rewrite
+    :parser parse-stop-at
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("parse")
+    :category :parse
+    :parser parse-parse-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("match" "unify")
+    :category :inspect
+    :parser parse-match-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("lisp" "ev") 
+    :category :system
+    :parser parse-eval-lisp
+    :evaluator cafeobj-eval-lisp-proc
+    :doc "
+")
+
+(define ("lispq" "evq")
+    :category :system
+    :parser parse-eval-lisp
+    :evaluator cafeobj-eval-lisp-q-proc
+    :doc "
+")
+
+(define ("make")
+    :category :decl-toplevel
+    :parser parse-make-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("in" "input")
+    :category :misc
+    :parser parse-input-command
+    :evaluator cafeobj-eval-input-proc
+    :doc "
+")
+
+(define ("save")
+    :category :io
+    :parser parse-save-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("restore")
+    :category :io
+    :parser parse-restore-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("reset")
+    :category :system
+    :parser parse-reset-command
+    :evaluator eval-ast
+    :doc (("reset"
+	   "
+remove declarations of user defined modules and views from the system.
+")))
+
+(define ("full" "full-reset") 
+    :doc ((("full reset" "full-reset") "reset system to initial status."))
+    :category :system
+    :parser parse-full-reset-command
+    :evaluator eval-ast)
+
+(define ("clean")
+    :category :rewrite
+    :parser identity
+    :evaluator cafeobj-eval-clear-memo-proc
+    :doc "
+")
+
+(define  ("prelude")
+    :category :library
+    :parser parse-prelude-command
+    :evaluator cafeobj-eval-prelude-proc
+    :doc "
+")
+
+(define ("let") 
+    :category :decl-toplevel
+    :parser process-let-declaration-form
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("imports")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+## `imports { <import-decl> }` ## {#imports}
+
+Block enclosing import of other modules (`protecting` etc). 
+Other statements are not allowed within the `imports` block.
+Optional structuring of the statements in a module.
+
+Related: [`signature`](#signature) [`axioms`](#axioms)
+  [`extending`](#extending)   [`including`](#including) 
+  [`protecting`](#protecting) [`using`](#using)
+")
+
+(define ("ex" "extending")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+## `extending ( <modexp> )` ## {#extending}
+
+Alias: `ex`
+
+imports the object specified by `modexp` into the current
+module, allowing models to be inflated, but not collapsing. 
+See [`module expression`](#moduleexpression) for format of `modexp`.
+
+Related: [`including`](#including) [`protecting`](#protecting) 
+	 [`using`](#using)
+")
+
+(define ("pr" "protecting")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("us" "using")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("inc" "including")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("[")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("*")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("bsort")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("op" "ops")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("bop" "bops")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("pred")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("bpred")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("dpred")		; only for pignose
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("dbpred")		; only for pignose
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("sig" "signature")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("axiom" "ax")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("axioms" "axs")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("ax")			; pignose
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("bax")			; pignose
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("goal")		; pignose
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("bgoal")		; pignose
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("#define")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+  
+(define ("var" "vars")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("pvar" "pvars")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("eq"  "ceq" "cq")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("beq" "bceq" "bcq")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("trans" "ctrans")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+    
+(define ("trns" "ctrns")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("rule" "crule")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("rl" "crl")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("btrans" "bctrans")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("brule" "bcrule")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("btrns" "bctrns")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("brl" "bcrl")
+    :category :module-element
+    :parser identity
+    :evaluator cafeobj-eval-module-element-proc
+    :doc "
+")
+
+(define ("open")
+    :category :proof
+    :parser parse-open-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("close")
+    :category :proof
+    :parser parse-close-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("start")
+    :category :proof
+    :parser parse-start-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("apply")
+    :category :proof
+    :parser parse-apply-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("choose") 
+    :category :proof
+    :parser parse-choose-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("inspect")
+    :category :proof
+    :parser parse-inspect-term-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("find")
+    :category :proof
+    :parser parse-find-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("show" "sh")
+    :category :inspect
+    :parser parse-show-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("set")
+    :category :switch
+    :parser parse-set-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("protect")
+    :category :system
+    :parser parse-protect-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("unprotect") 
+    :category :system
+    :parser parse-unprotect-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("select")
+    :category :proof
+    :parser parse-show-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("describe" "desc")
+    :category :inspect
+    :parser parse-show-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("autoload")
+    :category :library
+    :parser parse-autoload-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("provide") 
+    :category :library
+    :parser parse-provide-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("require") 
+    :category :library
+    :parser parse-require-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("pwd")
+    :category :misc
+    :parser parse-pwd-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("cd") 
+    :category :misc
+    :parser parse-cd-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("pushd")
+    :category :misc
+    :parser parse-pushd-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("popd")
+    :category :misc
+    :parser parse-popd-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("dirs")
+    :category :misc
+    :parser parse-dirs-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("ls")
+    :category :misc
+    :parser parse-ls-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("") 
+    :category :misc
+    :parser identity
+    :evaluator cafeobj-eval-control-d
+    :doc "
+")
+
+(define ("cont" "continue")
+    :category :rewrite
+    :parser parse-continue-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("look")
+    :category :inspect
+    :parser parse-look-up-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("names" "name")
+    :category :inspect
+    :parser parse-name-command
+    :evaluator eval-ast
+    :doc "
+show
+")
+
+
+(define ("scase")
+    :category :proof
+    :parser parse-case-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("sos" "passive")
+    :category :proof
+    :parser pignose-parse-sos
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("db")
+    :category :proof
+    :parser pignose-parse-db
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("clause")
+    :category :proof
+    :parser pignose-parse-clause
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("list")
+    :category :proof
+    :parser pignose-parse-list-command
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("flag")
+    :category :proof
+    :parser pignose-parse-flag
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("param")
+    :category :proof
+    :parser pignose-parse-param
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("option")
+    :category :proof
+    :parser pignose-parse-option
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("resolve")
+    :category :proof
+    :parser pignose-parse-resolve
+    :evaluator eval-ast
+    :doc "
+")
+
+(define  ("demod")
+    :category :proof
+    :parser pignose-parse-demod
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("save-option")
+    :category :proof
+    :parser pignose-parse-save-option
+    :evaluator eval-ast
+    :doc "
+")
+
+(define ("sigmatch")
+  :category :proof
+  :parser pignose-parse-sigmatch
+  :evaluator eval-ast
+  :doc "
+")
+
+(define  ("lex")
+    :category :proof
+    :parser pignose-parse-lex
+    :evaluator eval-ast
+    :doc "
+")
+
+(define (".")
+    :category :misc
+    :parser identity
+    :evaluator cafeobj-nop
+    :doc "
+")
+
+
+;;;
+)					; end eval-when
+;;; EOF
diff --git a/cafeobj/creader-.lisp b/cafeobj/creader-.lisp
deleted file mode 100644
index fe386fe..0000000
--- a/cafeobj/creader-.lisp
+++ /dev/null
@@ -1,644 +0,0 @@
-;;;-*- Mode: Lisp; Syntax:CommonLisp; Package:CHAOS; Base:10 -*-
-;;; $Id: creader.lisp,v 1.15 2010-08-09 00:43:37 sawada Exp $
-(in-package :chaos)
-#-:chaos-debug
-(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
-#+:chaos-debug
-(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
-
-#|=============================================================================
-System:CHAOS
-Module: cafeobj
-File: creader.lisp
-==============================================================================|#
-
-;;;=============================================================================
-;;; Schema based generalized reader based on OBJ3 implementation.
-;;;=============================================================================
-
-;;; TOP-LEVEL module parser invokes 'reader' with schemas for modules
-
-(defun cafeobj-parse ()
-  (reader 'Top-form *cafeobj-schemas*))
-
-;;; SCHEMA
-;;;  schema for top-level of CafeOBJ ===========================================
-
-;;;=============================================================================
-;;; CafeOBJ Schemas
-;;;-----------------------------------------------------------------------------
-
-(eval-when (eval compile load)
-
-;;;-----------------------------------------------------------------------------
-;;; SORT/SUBSORT DECLARATION
-;;;-----------------------------------------------------------------------------
-
-;;; VISIBLE SORTS
-
-  (defparameter SortDeclaration
-      ' (|[| (:upto (< |,| |]|) :sorts)
-             :append (:seq-of (:one-of (<) (|,|))
-                              (:upto (< |,| |]|) :sorts))
-             |]|))
-
-;;; HIDDEN SORTS
-
-  (defparameter HSortDeclaration
-      '(*
-        (|[| (:upto (< |,| |]|) :sorts)
-         :append (:seq-of (:one-of (<) (|,|))
-                  (:upto (< |,| |]|) :sorts))
-         |]|)
-        *))
-
-  (defparameter HRCSortDeclaration
-      '(*record :symbol (:optional (:! Supers))
-        |{|
-        (:optional (:! Sv-pairs))
-        |}|)
-    )
-
-;;; BUILTIN SORT
-
-  (defparameter BSortDeclaration
-      '(bsort :symbol (:call (read))))
-
-;;; BUILTIN HIDDEN SORT
-
-  (defparameter BHSortDeclaration
-      '(hbsort :symbol (:call (read))))
-
-;;;-----------------------------------------------------------------------------
-;;; OPERATOR DECLARATION
-;;;-----------------------------------------------------------------------------
-
-;;; GENERAL OPERATORs
-
-  (defparameter OperatorDeclaration
-      '((:+ op ops) (:seq-of :opname) |:| :sorts -> :sort
-        (:if-present
-         |{| (:many-of
-              ((:+ assoc comm idem associative commutative idempotent))
-              (|id:| :chaos-item)
-              (|identity:| :chaos-item)
-              (|idr:| :chaos-item)
-              (|identity-rules:| :chaos-item)
-              ((:pred general-read-numberp))
-              ((:+ prec precedence |prec:| |pecedence:|) :int)
-              (|(| (:seq-of :int) |)|)
-              ((:+ strat strategy |strat:| |strategy:|)
-               |(| (:seq-of :int) |)|)
-              ((:+ l-assoc r-assoc left-associative right-associative))
-              ((:+ constr constructor))
-              ((:+ coherent beh-coherent))
-              (memo)
-              )
-         |}|
-         )))
-
-;;; BEHAVIOURAL OPERATOR DECLARATION
-
-  (defparameter BOperatorDeclaration
-      '((:+ bop bops) (:seq-of :opname) |:| :sorts -> :sort
-        (:if-present
-         |{| (:many-of
-              ((:+ assoc comm idem associative commutative idempotent))
-              (|id:| :chaos-item)
-              (|identity:| :chaos-item)
-              (|idr:| :chaos-item)
-              (|identity-rules:| :chaos-item)
-              ((:pred general-read-numberp))
-              ((:+ prec precedence |prec:| |pecedence:|) :int)
-              (|(| (:seq-of :int) |)|)
-              ((:+ strat strategy |strat:| |strategy:|)
-               |(| (:seq-of :int) |)|)
-              ((:+ l-assoc r-assoc left-associative right-associative))
-              ((:+ constr constructor))
-              (memo)
-              )
-         |}|
-         )))
-
-;;; PREDICATE -- short hand for bool-valued ops.
-
-  (defparameter PredicateDeclaration
-      '(pred (:seq-of :opname) |:|
-        (:upto (op ops bop bops |[| pred preds bpred bpreds hidden signature sig
-                axioms ax axiom imports dpred
-                |{| |}| |.| -- ** --> **> class record eq rule rl ceq crule crl
-                bq bcq beq bceq brule brl bcrule bcrl trans trns btrans btrns
-                bctrans bctrns fax bfax
-                var vars parse ev evq lisp lispq let)
-         :sorts)
-        (:if-present
-         |{| (:many-of
-              ((:+ assoc comm idem associative commutative idempotent))
-              (|id:| :chaos-item)
-              (|identity:| :chaos-item)
-              (|idr:| :chaos-item)
-              (|identity-rules:| :chaos-item)
-              ;; ((:pred general-read-numberp))
-              ((:+ prec precedence |prec:| |pecedence:|) :int)
-              (|(| (:seq-of :int) |)|)
-              ((:+ strat strategy |strat:| |strategy:|)
-               |(| (:seq-of :int) |)|)
-              ((:+ l-assoc r-assoc left-associative right-associative))
-              ((:+ constr constructor))
-              ((:+ coherent beh-coherent))
-              ((:+ meta-demod demod))
-              (memo)
-              )
-         |}|
-         )))
-
-  (defparameter BPredicateDeclaration
-      '(bpred (:seq-of :opname) |:|
-        (:upto (op ops bop bops |[| pred preds bpred bpreds hidden signature sig
-                axioms ax axiom imports 
-                |{| |}| |.| -- ** --> **> class record eq rule rl ceq crule crl
-                bq bcq beq bceq brule brl bcrule bcrl trans trns btrans btrns
-                bctrans bctrns fax bfax
-                var vars parse ev evq lisp lispq let)
-         :sorts)
-        (:if-present
-         |{| (:many-of
-              ((:+ assoc comm idem associative commutative idempotent))
-              (|id:| :chaos-item)
-              (|identity:| :chaos-item)
-              (|idr:| :chaos-item)
-              (|identity-rules:| :chaos-item)
-              ;; ((:pred general-read-numberp))
-              ((:+ prec precedence |prec:| |pecedence:|) :int)
-              (|(| (:seq-of :int) |)|)
-              ((:+ strat strategy |strat:| |strategy:|)
-               |(| (:seq-of :int) |)|)
-              ((:+ l-assoc r-assoc left-associative right-associative))
-              ((:+ constr constructor))
-              ((:+ coherent beh-coherent))
-              (memo)
-              ((:+ demod meta-demod))
-              )
-         |}|
-         )))
-  
-;;; OPERATOR ATTRIBUTES
-;;; Now almost obsolate.
-
-  (defparameter OperatorAttribute
-      '((:+ attr attrs) (:seq-of :opname)
-        |{|
-        (:many-of
-         ((:+ assoc comm idem associative commutative idempotent))
-         (|id:| :chaos-item)
-         (|identity:| :chaos-item)
-         (|idr:| :chaos-item)
-         (|identity-rules:| :chaos-item)
-         ;; ((:pred general-read-numberp))
-         ((:+ prec precedence |prec:| |pecedence:|) :int)
-         (|(| (:seq-of :int) |)|)
-         ((:+ strat strategy |strat:| |strategy:|) |(| (:seq-of :int) |)|)
-         ((:+ l-assoc r-assoc))
-         ;; ((:+ constr constructor))
-         (memo)
-         )
-        |}|))
-
-;;;-----------------------------------------------------------------------------
-;;; RECORD DECLARATION
-;;; *NOTE* class is not part of CafeOBJ language.
-;;;-----------------------------------------------------------------------------
-
-  (defparameter R-C-Declaration
-      '((:+ record class) :symbol (:optional (:! Supers)) |{|
-        (:optional (:! Sv-pairs))
-        |}|))
-
-;;;-----------------------------------------------------------------------------
-;;; LET
-;;;-----------------------------------------------------------------------------
-
-  (defparameter LetDeclaration
-      '(let :symbol (:optional |:| :sort) = :term |.|))
-
-;;;-----------------------------------------------------------------------------
-;;; VARIABLE DECLARATION
-;;;-----------------------------------------------------------------------------
-  (defparameter VarDeclaration
-      '(var :symbol |:| :sort))
-  (defparameter VarsDeclaration
-      '(vars :symbols |:| :sort))
-  (defparameter PVarDeclaration
-      '(pvar :symbol |:| :sort))
-  (defparameter PVarsDeclaration
-      '(pvars :symbols |:| :sort))
-
-;;;-----------------------------------------------------------------------------
-;;; MACRO
-;;;-----------------------------------------------------------------------------
-  (defparameter MacroDeclaration
-      '(|#define| :term |::=| :term |.|))
-
-;;;-----------------------------------------------------------------------------
-;;; AXIOMS
-;;;-----------------------------------------------------------------------------
-
-;;; EQUATION
-
-  (defparameter EqDeclaration
-      '(eq (:optional |[| (:seq-of :symbol (:upto (|]| |:|)))) :term = :term |.|))
-  (defparameter BEqDeclaration
-      '((:+ beq bq) :term = :term |.|))
-  (defparameter CEQDeclaration
-      '((:+ ceq cq) :term = :term if :term |.|))
-  (defparameter BCEQDeclaration
-      '((:+ bceq bcq) :term = :term if :term |.|))
-  (defparameter FoplAXDeclaration
-      '((:+ fax bfax ax bax frm bfrm) :term |.|))
-  (defparameter FoplGoalDeclaration
-      '((:+ goal bgoal) :term |.|))
-
-;;; STATE TRANSITION
-
-  (defparameter RlDeclaration
-      '((:+ rule rl trans trns) :term => :term |.|))
-  (defparameter BRLDeclaration
-      '((:+ brule brl btrans btrns) :term => :term |.|))
-  (defparameter CRLDeclaration
-      '((:+ crule crl ctrans ctrns) :term => :term if :term |.|))
-  (defparameter BCRLDeclaration
-      '((:+ bcrule brl bctrans bctrns) :term => :term if :term |.|))
-
-;;;-----------------------------------------------------------------------------
-;;; IMPORTATIONS
-;;;-----------------------------------------------------------------------------
-
-  (defparameter ExDeclaration
-      '((:+ ex extending) |(| :modexp |)|))
-  (defparameter PrDeclaration
-      '((:+ pr protecting) |(| :modexp |)|))
-  (defparameter UsDeclaration
-      '((:+ us using) |(| :modexp |)|))
-  (defparameter IncDeclaration
-      '((:+ inc including) |(| :modexp |)|))
-
-  )
-
-;;;-----------------------------------------------------------------------------
-;;; THE SCHEME OF WHOLE ALLOWABLE INPUTS
-;;;-----------------------------------------------------------------------------
-
-(eval-when (eval load)
-  (setq *cafeobj-schemas*
-    '(
-      (Top-form
-       (:one-of
-        (;; MODULE : Its Constructs
-         ;; --------------------------------------------------
-         (:+ mod module module* module! mod* mod! 
-             |sys:mod| |sys:mod*| |sys:mod!|
-             |sys:module| |sys:module*| |sys:module!|
-             |hwd:module!| |hwd:module*| |hwd:module|
-             ots |sys:ots| |hwd:ots|
-             )
-         :symbol                        ; (:optional (:! Params))
-         (:if-present (:+ \( \[) (:! Param) :append (:seq-of |,| (:! Param))
-                      (:+ \) \]))
-         (:if-present principal-sort :sort)
-         ;; (:if-present psort :sort)
-         |{|
-         (:many-of
-
-          ;; MODULE IMPORTATIONS
-          ;; *NOTE*  imports { ... } is not in MANUAL, and does not have
-          ;;         translater to Chaos now.
-          ((:+ imports import)
-           |{|
-           (:many-of
-            #.ExDeclaration
-            #.PrDeclaration
-            #.UsDeclaration
-            #.IncDeclaration
-            ((:+ --> **>) :comment)
-            ((:+ -- **) :comment)
-            )
-           |}|)
-          #.ExDeclaration
-          #.PrDeclaration
-          #.UsDeclaration
-          #.IncDeclaration
-
-          ;; SIGNATURE
-          ((:+ sig signature) |{|
-                              (:many-of
-                               #.BSortDeclaration
-                               #.BHSortDeclaration
-                               #.HSortDeclaration
-                               #.SortDeclaration
-                               #.OperatorDeclaration
-                               #.BOperatorDeclaration
-                               #.PredicateDeclaration
-                               #.BPredicateDeclaration
-                               #.OperatorAttribute
-                               #.R-C-Declaration
-                               ((:+ --> **>) :comment)
-                               ((:+ -- **) :comment)
-                               )
-                              |}|)
-
-          ;; AXIOMS
-          ((:+ axiom axioms axs) |{|
-                                 (:many-of
-                                  #.LetDeclaration
-                                  #.MacroDeclaration
-                                  #.VarDeclaration
-                                  #.VarsDeclaration
-                                  #.EqDeclaration
-                                  #.CeqDeclaration
-                                  #.RlDeclaration
-                                  #.CRlDeclaration
-                                  #.BeqDeclaration
-                                  #.BCeqDeclaration
-                                  #.BRLDeclaration
-                                  #.BCRLDeclaration
-                                  #.FoplAXDeclaration
-                                  #.FoplGoalDeclaration
-                                  ((:+ --> **>) :comment)
-                                  ((:+ -- **) :comment)
-                                  )
-                                 |}|)
-
-          ;; Module elements without signature/axioms.
-          #.BSortDeclaration
-          #.BHSortDeclaration
-          #.SortDeclaration
-          #.HSortDeclaration
-          #.BHSortDeclaration
-          #.R-C-Declaration
-          #.OperatorDeclaration
-          #.BOperatorDeclaration
-          #.PredicateDeclaration
-          #.BPredicateDeclaration
-          #.OperatorAttribute
-          #.LetDeclaration
-          #.MacroDeclaration
-          #.VarDeclaration
-          #.VarsDeclaration
-          #.EqDeclaration
-          #.BEqDeclaration
-          #.CeqDeclaration
-          #.BCeqDeclaration
-          #.RlDeclaration
-          #.CRlDeclaration
-          #.BRlDeclaration
-          #.BCRLDeclaration
-          #.FoplAXDeclaration
-          #.FoplGoalDeclaration
-          ((:+ --> **>) :comment)
-          ((:+ -- **) :comment)
-
-          ;; Misc elements.
-          (parse :term |.|)
-          ((:+ ev lisp evq lispq) (:call (read)))
-          ;; allow sole ".", and do nothing
-          (|.|)
-          )
-         |}|
-         )                              ; end module
-
-        ;; VIEW DECLARATION
-        ;; --------------------------------------------------
-        (view :symbol 
-              :modexp
-              |}|)
-
-        ;; MAKE
-        ;; --------------------------------------------------
-        (make :symbol |(| :modexp |)|)
-
-        ;; TOP LEVEL COMMANDS
-        ;; --------------------------------------------------
-        ((:+ reduce red execute exec exec! execute! breduce bred)
-         (:if-present  in :modexp |:|) (:seq-of :term) |.|)
-        (tram (:+ compile execute exec red reduce reset)
-              (:if-present in :modexp |:|)
-              (:seq-of :term) |.|)
-        ((:+ cbred)
-         (:if-present in :modexp |:|)
-         (:seq-of :term) |.|)
-        (version)
-        ;;
-        (autoload :symbol :symbol)
-        ;; (stop at :term |.|)
-        ;; ((:+ rwt) limit :symbol)
-        (test (:+ reduction red execution exec) (:if-present in :modexp |:|)
-              (:seq-of :term)
-              (:+ |:expect| |expect:| expect) (:seq-of :term) |.|)
-        ;; ((:+ match unify) (:seq-of :term) (:+ to :to) (:seq-of :term) |.|)
-        (match :term (:+ to with) :term |.|)
-        (unify :term (:+ to with) :term |.|)
-        ;; (call-that :symbol)
-        ;; ((:+ language lang) :symbol)
-        ((:+ input in) :symbol)
-        (check (:seq-of :top-opname))
-        (regularize (:seq-of :top-opname))
-        (save :symbol)
-        (restore :symbol)
-        (prelude :symbol)
-        (save-system :symbol)
-        (protect (:seq-of :top-opname))
-        (unprotect (:seq-of :top-opname))
-        (clean memo)
-        (reset)
-        (full-reset)
-        (full reset)
-        ((:+ --> **>) :comment)
-        ((:+ -- **) :comment)
-        (parse (:if-present  in :modexp |:|) (:seq-of :term) |.|)
-        ((:+ lisp ev eval evq lispq)
-         (:call (read)))
-        (;; (:+ show sh set select describe desc) ; do 
-         set
-         (:seq-of :top-opname))
-        ;; (select :modexp :args)
-        ((:+ show sh select describe desc) :args)
-        (trans-chaos (:seq-of :top-opname))
-
-        ;; module elements which can appear at top(iff a module is opened.)
-
-        #.PrDeclaration
-        #.ExDeclaration
-        #.UsDeclaration
-        #.IncDeclaration
-        #.BSortDeclaration
-        #.BHSortDeclaration
-        #.HSortDeclaration
-        #.SortDeclaration
-        #.OperatorDeclaration
-        #.BOperatorDeclaration
-        #.PredicateDeclaration
-        #.BPredicateDeclaration
-        #.LetDeclaration
-        #.MacroDeclaration
-        #.VarDeclaration
-        #.VarsDeclaration
-        #.PVarDeclaration
-        #.PVarsDeclaration
-        #.EqDeclaration
-        #.CEqDeclaration
-        #.BEqDeclaration
-        #.BCEqDeclaration
-        #.RlDeclaration
-        #.CRlDeclaration
-        #.BRlDeclaration
-        #.BCRLDeclaration
-        #.FoplAXDeclaration
-        #.FoplGoalDeclaration
-        ;; theorem proving stuff.
-        ;; (open (:seq-of :top-opname))
-        (open :modexp |.|)
-        (close)
-        (start :term |.|)
-        ;; trace/untrace
-        ((:+ trace untrace) :symbol)
-        ;; apply
-        (apply (:one-of-default
-                (:symbol (:upto
-                          (within at)
-                          (:optional with :symbol
-                                     = (:upto (|,| within at) :term)
-                                     :append
-                                     (:seq-of |,| :symbol
-                                              = (:upto (|,| within at) :term))))
-                         (:+ within at)
-                         (:one-of
-                          ((:+ top it term subterm))
-                          ((:+ |(| |{| |[|)
-                           :unread
-                           ((:! Selector))
-                           (:seq-of of ((:! Selector)))
-                           |.|)))
-                (?)))
-        ;;
-        (choose (:one-of
-                 ((:+ top term subterm))
-                 ((:+ |(| |{| |[|)
-                  :unread
-                  ((:! Selector))
-                  (:seq-of of ((:! Selector)))
-                  |.|)))
-
-        (find (:+ rule -rule +rule rules -rules +rules))
-
-        ;; RWL related commands
-        ((:+ cont continue) :args)
-        
-        ;; PROVIDE/REQUIRE
-        (provide :symbol)
-        (require :top-term)
-        (autoload :symbol :symbol)
-
-        ;; PigNose commands
-        #+:bigpink (db reset)
-        #+:bigpink ((:+ sos passive) (:+ = + -)
-                                     |{|
-                                     (:upto (|,| |}|) :sorts)
-                                     :append (:seq-of |,|
-                                                      (:upto (|}| |,|) :sorts))
-                                     |}|)
-        #+:bigpink (list
-                    (:+ axiom axioms
-                        sos usable
-                        flag param flags parameter parameters
-                        option options passive
-                        demod demodulator demodulators))
-        #+:bigpink (clause :term |.|)
-        #+:bigpink (option (:one-of (reset)
-                                    (= :symbol)))
-        #+:bigpink ((:+ save-option save-options) :symbol)
-        #+:bigpink (flag |(| :symbol |,| (:+ on off set clear) |)|)
-        #+:bigpink (param |(| :symbol |,| :int |)|)
-        #+:bigpink (resolve :args)
-        #+:bigpink (demod (:if-present  in :modexp |:|) (:seq-of :term) |.|)
-        #+:bigpink (sigmatch |(| :modexp |)| (:+ to with) |(| :modexp |)|)
-
-        #+:bigpink (lex |(|
-                        (:upto (|,| |)|) :opname)
-                        :append (:seq-of |,|
-                                         (:upto (|,| |)|) :opname))
-                        |)|)
-        ;; misc toplevel commands
-        (eof)
-        #-CMU (#\^D)
-        #+CMU (#\)
-        (prompt (:seq-of :top-opname))
-        ((:+ quit q |:q| |:quit|))
-        (cd :args)
-        (pushd :args)
-        (popd :args)
-        (dirs)
-        ;; #-(or GCL LUCID CMU) (ls :symbol)
-        ;; #+(or GCL LUCID CMU) 
-        ;; (ls :top-opname)
-        (ls :args)
-        (dribble :symbol)
-        (pwd)
-        (! :top-term)                   ; shell escape
-        (? :args)                       ; help/messege description
-        (?? :args)                      ; detailed help
-        (|.|)
-        (chaos :args)
-        ))                              ; end Top-Form
-
-      ;; some separated definitions of non-terminals.
-      ;; --------------------------------------------------
-      ;; subterm specifier
-      
-      (Selector
-       (:one-of
-        ;; (term) (top) (subterm)
-        (|{| :int :append (:seq-of |,| :int) |}|)
-        (|(| (:seq-of :int) |)|)
-        (\[ :int (:optional |..| :int) \])))
-
-      ;; parameter part
-      ;; (Params (\[ (:! Param) :append (:seq-of |,| (:! Param)) \]))
-      (Param 
-       (:one-of-default
-        (:symbols |::| (:upto (|,| \] \)) :modexp))
-        ((:+ ex extending us using pr protecting inc including)
-         :symbols |::| (:upto (|,| \] \)) :modexp))))
-
-      ;; importation modexp
-      #||
-      (ImportModexp
-       (:symbol :modexp))
-      (IM (:one-of-default
-           (:modexp)
-           (|::| :modexp)))
-      ||#
-      ;; (sortConst
-      ;;  (:one-of-default
-      ;;   (:sorts)
-      ;;  (:symbol = { :term |:| :sorts })))
-
-      ;; super reference.
-      (Supers (\[ (:! Super) :append (:seq-of |,| (:! Super)) \]))
-      (Super ((:upto (|,| \]) :super)))
-      ;; slot/value pairs
-      (SV-Pairs
-       ((:! Sv-pair) :append  (:seq-of (:! Sv-pair)) ;(:seq-of |,| (:! Sv-pair))
-        ))
-      (Sv-Pair
-       (:one-of-default
-        (:symbol (:upto (|}|))
-         (:one-of (|:| :sort)
-                  (= |(| :term |)| |:| :sort)))
-        ((:+ -- **) :comment)
-        ((:+ --> **>) :comment))
-       )
-      ))
-  )
-
-
-;;; EOF
diff --git a/cafeobj/declarations.lisp b/cafeobj/declarations.lisp
new file mode 100644
index 0000000..d787006
--- /dev/null
+++ b/cafeobj/declarations.lisp
@@ -0,0 +1,201 @@
+;;;-*- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp -*-
+#|==============================================================================
+                            System: CHAOS
+                           Module: cafeobj
+                       File: declarations.lisp
+==============================================================================|#
+(in-package :chaos)
+#-:chaos-debug
+(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
+#+:chaos-debug
+(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
+
+;;; ----------------------------------------
+;;; register declarations keywords
+;;; ----------------------------------------
+(eval-when (:execute :load-toplevel)
+  (clrhash *cafeobj-declarations*)
+  
+;;; 
+;;; All the Declaration forms --------------------------------------------------------------
+;;;
+
+(define ("bsort")
+    :type :inner-module
+    :category :signature
+    :parser process-bsort-declaration
+    :evaluator eval-ast)
+
+(define ("[")
+    :type :inner-module
+    :category :signature
+    :parser process-sort-and-subsort-form
+    :evaluator eval-ast)
+
+(define ("hidden" "*")
+    :type :inner-module
+    :category :signature
+    :parser process-hidden-sort-form
+    :evaluator eval-ast)
+
+(define ("op")
+    :type :inner-module
+    :category :signature 
+    :parser process-operator-declaration-form
+    :evaluator eval-ast)
+
+(define ("ops")
+    :type :inner-module
+    :category :signature 
+    :parser process-operators-declaration-form
+    :evaluator eval-ast)
+
+(define ("bop")
+    :type :inner-module
+    :category :signature
+    :parser process-operator-declaration-form
+    :evaluator eval-ast)
+
+(define ("bops")
+    :type :inner-module
+    :category :signature 
+    :parser process-boperators-declaration-form
+    :evaluator eval-ast)
+
+(define ("pred")
+    :type :inner-module
+    :category :signature
+    :parser process-predicate-declaration-form
+    :evaluator eval-ast)
+
+(define ("dpred")
+    :type :inner-module
+    :category :signature 
+    :parser process-predicate-declaration-form
+    :evaluator eval-ast)
+              
+(define ("bpred")
+    :type :inner-module
+    :category :signature 
+    :parser process-predicate-declaration-form
+    :evaluator eval-ast)
+              
+(define ("dbpred")
+    :type :inner-module
+    :category :signature 
+    :parser process-predicate-declaration-form
+    :evaluator eval-ast)
+              
+(define ("rec" "record")
+    :type :inner-module
+    :category :signature 
+    :parser process-record-declaration-form
+    :evaluator eval-ast)
+
+(define ("let")
+    :type :inner-module
+    :category :axiom
+    :parser process-let-declaration-form
+    :evaluator eval-ast)
+
+(define ("#define")
+    :type :inner-module
+    :category :axiom
+    :parser process-macro-declaration-form
+    :evaluator eval-ast)
+
+(define ("eq" "cq" "ceq" "rule" "rl" "crl" "crule" "trans" "ctrans" "trns" "ctrns"
+	       "beq" "bceq" "brule" "brl" "bcrule" "bcrl" "btrans" "btrns"
+	       "bctrans" "bctrns")
+    :type :inner-module
+    :category :axiom
+    :parser process-axiom-form
+    :evaluator eval-ast)
+
+(define ("var" "vars")
+    :type :inner-module
+    :category :axiom
+    :parser process-variable-declaration-form
+    :evaluator eval-ast)
+              
+(define ("pvar" "pvars")
+    :type :inner-module
+    :category :axiom
+    :parser process-pseud-variable-declaration-form
+    :evaluator eval-ast)
+              
+(define ("fax" "bfax" "ax" "bax" "frm" "bfrm")
+    :type :inner-module
+    :category :axiom
+    :parser pignose-process-fax-proc
+    :evaluator eval-ast)
+
+(define ("goal" "bgoal")
+    :type :inner-module
+    :category :axiom
+    :parser pignose-process-goal-proc
+    :evaluator eval-ast)
+              
+(define ("imports" "import")
+    :type :inner-module
+    :category :signature
+    :parser parse-imports-form
+    :evaluator eval-ast)
+
+(define ("pr" "protecting" "ex" "extending" "us" "using" "inc" "including")
+    :type :inner-module
+    :category :import
+    :parser process-importation-form
+    :evaluator eval-ast)
+
+(define ("--" "**")
+    :type :inner-module
+    :category :ignore
+    :parser parse-decl-do-nothing
+    :evaluator eval-decl-do-nothing)
+
+(define ("-->")
+    :type :inner-module
+    :category :ignore
+    :parser parse-dynamic-comment-1
+    :evaluator eval-decl-do-nothing)
+
+(define ("**>")
+    :type :inner-module
+    :category :ignore
+    :parser parse-dynamic-comment-2
+    :evaluator eval-decl-do-nothing)
+
+(define ("ev" "lisp" "evq" "lispq")
+    :type :inner-module
+    :category :ignore
+    :parser process-ev-lisp-form
+    :evaluator eval-decl-do-nothing)
+
+(define ("eval")
+    :type :inner-module
+    :category :misc
+    :parser parse-eval-form
+    :evaluator eval-ast)
+
+(define ("sig" "signature")
+    :type :inner-module
+    :category :signature
+    :parser process-signature
+    :evaluator eval-ast)
+
+(define ("axioms" "axiom" "axs")
+    :type :inner-module
+    :category :axiom
+    :parser process-axioms-declaration
+    :evaluator eval-ast)
+
+(define (".")                    ; sole dots
+    :type :inner-module
+    :category :ignore
+    :parser parse-decl-do-nothing
+    :evaluator eval-decl-do-nothing)
+
+;;;
+)					; end eval-when
+;;; EOF
diff --git a/cafeobj/defcommand.lisp b/cafeobj/defcommand.lisp
deleted file mode 100644
index ac19dcc..0000000
--- a/cafeobj/defcommand.lisp
+++ /dev/null
@@ -1,841 +0,0 @@
-;;;-*- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp -*-
-#|==============================================================================
-                            System: CHAOS
-                           Module: cafeobj
-                         File: defcommand.lisp
-==============================================================================|#
-(in-package :chaos)
-#-:chaos-debug
-(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
-#+:chaos-debug
-(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
-
-;;; ----------------------------------------
-;;; register commands & declaration keywords
-;;; ----------------------------------------
-(eval-when (:execute :load-toplevel)
-
-  (clrhash *cafeobj-commands*)
-  (clrhash *cafeobj-declarations*)
-  
-;;;
-;;; declarations/commands which can apper at top-level --------------------------------------
-;;;  
-
-(defcom ("mod" "module" "module*" "mod*" "module!" "mod!" "sys:mod!" "sys:module!" "sys:mod*" "sys:module*")
-  "declares module.~%module <Name> [<Parameters>] [<PrincipalSort>] { <ModuleBody> }."
-  :toplevel-declaration
-  process-module-declaration-form
-  eval-ast)
-
-(defcom ("view")
-    "declares view.~%view <Name> { <Map> ... }"
-  :topelevel-declaration
-  process-view-declaration-form
-  eval-ast)
-
-(defcom ("check")
-    "check current module's various properties.~
-~%check regularity : checks whether module's signagure is regular or not"
-  :checker
-  parse-check-command
-  eval-ast)
-
-(defcom ("regularize")
-    "destructively makes current module's signature to be regular by adding sorts and operators."
-  :module
-  parse-regularize-command
-  eval-ast)
-
-(defcom ("exec" "execute")
-    "exec [in <Modexpr> :] <Term> . ~%Rewrite <Term> by '(c)trans' axioms of the module."
-  :rewrite
-  parse-exec-command
-  eval-ast)
-
-(defcom ("red" "reduce")
-    "reduce [in <Modexpr> :] <Term> . ~%Rewrite <Term> by axioms of the module."
-  :rewrite
-  parse-reduce-command
-  eval-ast)
-
-(defcom ("exec!" "execute!")
-    "exec! [in <Modexpr> :] <Term> . "
-  :rewrite
-  parse-exec+-command
-  eval-ast)
-
-(defcom ("bred" "breduce")
-    ""
-  :rewrite
-  parse-bred-command
-  eval-ast)
-
-(defcom ("version")
-    "prints version number of the system."
-  :misc
-  parse-version-command
-  princ)
-
-(defcom ("cbred")
-    ""
-  :rewrite
-  parse-cbred-command
-  eval-ast)
-
-(defcom  ("stop")
-    ""
-  :rewrite
-  parse-stop-at
-  eval-ast)
-
-(defcom ("parse")
-    ""
-  :inspect
-  parse-parse-command
-  eval-ast)
-
-(defcom ("match" "unify")
-    ""
-  :inspect
-  parse-match-command
-  eval-ast)
-
-(defcom ("lisp" "ev") 
-    ""
-  :system
-  parse-eval-lisp
-  cafeobj-eval-lisp-proc)
-
-(defcom ("lispq" "evq")
-    ""
-  :system
-  parse-eval-lisp
-  cafeobj-eval-lisp-q-proc)
-
-;;; (defcom ("eval")
-;;;    ""
-;;;  :system
-;;;  parse-meta-eval
-;;;  eval-ast)
-
-(defcom ("make")
-    ""
-  :toplevel-decl
-  parse-make-command
-  eval-ast)
-
-(defcom  ("in" "input")
-    ""
-  :io
-  parse-input-command
-  cafeobj-eval-input-proc)
-
-(defcom ("save")
-    ""
-  :io
-  parse-save-command
-  eval-ast)
-
-(defcom ("restore")
-    ""
-  :io
-  parse-restore-command
-  eval-ast)
-
-(defcom ("reset")
-    ""
-  :system-state
-  parse-reset-command
-  eval-ast)
-
-(defcom ("full" "full-reset") 
-    ""
-  :system-state
-  parse-full-reset-command
-  eval-ast)
-
-(defcom ("clean")
-    ""
-  :rewrite
-  identity
-  cafeobj-eval-clear-memo-proc)
-
-(defcom  ("prelude")
-    ""
-  :library
-  parse-prelude-command
-  cafeobj-eval-prelude-proc)
-
-(defcom ("let") 
-    ""
-  :toplevel-declaration
-  process-let-declaration-form
-  eval-ast)
-
-(defcom ("--" "**")
-    ""
-  :toplevel-declaration
-  parse-comment-command
-  identity)
-
-(defcom ("-->" "**>")
-    ""
-  :toplevel-declaration
-  parse-comment-command
-  eval-ast)
-
-(defcom ("imports")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("ex" "extending")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("pr" "protecting")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("us" "using")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("inc" "including")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("[")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("*")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("bsort")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("op" "ops")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("bop" "bops")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("pred")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("bpred")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("dpred")		; only for pignose
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("dbpred")		; only for pignose
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("sig" "signature")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("axiom" "ax")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("axioms" "axs")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("ax")			; pignose
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("bax")			; pignose
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("goal")		; pignose
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("bgoal")		; pignose
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("#define")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-  
-(defcom ("var" "vars")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("pvar" "pvars")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("eq"  "ceq" "cq")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("beq" "bceq" "bcq")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("trans" "ctrans")
-    ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-    
-(defcom ("trns" "ctrns")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("rule" "crule")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("rl" "crl")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("btrans" "bctrans")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("brule" "bcrule")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("btrns" "bctrns")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("brl" "bcrl")
-        ""
-  :module-element
-  identity
-  cafeobj-eval-module-element-proc)
-
-(defcom ("open")
-    ""
-  :proof
-  parse-open-command
-  eval-ast)
-
-(defcom ("close")
-    ""
-  :proof
-  parse-close-command
-  eval-ast)
-
-(defcom ("start")
-    ""
-  :proof
-  parse-start-command
-  eval-ast)
-
-(defcom ("apply")
-    ""
-  :proof
-  parse-apply-command
-  eval-ast)
-
-(defcom  ("choose") 
-    ""
-  :proof
-  parse-choose-command
-  eval-ast)  
-
-(defcom ("inspect")
-    ""
-  :proof
-  parse-inspect-term-command
-  eval-ast)
-
-(defcom  ("find")
-    ""
-  :proof
-  parse-find-command
-  eval-ast)
-
-(defcom  ("show" "sh")
-    ""
-  :inspect
-  parse-show-command
-  eval-ast)
-
-(defcom  ("set")
-    ""
-  :switch
-  parse-set-command
-  eval-ast)
-
-(defcom ("protect")
-    ""
-  :system-status
-  parse-protect-command
-  eval-ast)
-
-(defcom ("unprotect") 
-    ""
-  :system-status
-  parse-unprotect-command
-  eval-ast)
-
-(defcom ("select")
-    ""
-  :proof
-  parse-show-command
-  eval-ast)
-
-(defcom ("describe" "desc")
-    ""
-  :inspect
-  parse-show-command
-  eval-ast)
-
-(defcom  ("autoload")
-    ""
-  :library
-  parse-autoload-command
-  eval-ast)
-
-(defcom  ("provide") 
-    ""
-  :library
-  parse-provide-command
-  eval-ast)
-
-(defcom  ("require") 
-    ""
-  :library
-  parse-require-command
-  eval-ast)
-
-(defcom ("??" "?")
-    ""
-  :help
-  identity
-  cafeobj-top-level-help)
-
-(defcom  ("dribble")
-    ""
-  :misc
-  parse-dribble-command
-  eval-ast)
-
-(defcom  ("pwd")
-    ""
-  :misc
-  parse-pwd-command
-  eval-ast)
-
-(defcom  ("cd") 
-    ""
-  :misc
-  parse-cd-command
-  eval-ast)
-
-(defcom ("pushd")
-    ""
-  :misc
-  parse-pushd-command
-  eval-ast)
-
-(defcom  ("popd")
-    ""
-  :misc
-  identity
-  parse-pushd-command)
-
-(defcom  ("dirs")
-    ""
-  :misc
-  parse-dirs-command
-  eval-ast)
-
-(defcom ("ls")
-    ""
-  :misc
-  parse-ls-command
-  eval-ast)
-
-(defcom ("!")
-    ""
-  :misc
-  parse-shell-command
-  eval-ast)
-
-(defcom ("") 
-    ""
-  :misc
-  identity
-  cafeobj-eval-control-d)
-
-(defcom ("cont" "continue")
-    ""
-  :rewrite
-  parse-continue-command
-  eval-ast)
-
-(defcom ("look")
-    ""
-  :inspect
-  parse-look-up-command
-  eval-ast)
-
-(defcom ("names" "name")
-    ""
-  :inspect
-  parse-name-command
-  eval-ast)
-
-(defcom ("scase")
-    ""
-  :proof
-  parse-case-command
-  eval-ast)
-
-(defcom ("sos" "passive")
-    ""
-  :proof
-  pignose-parse-sos
-  eval-ast)
-
-(defcom ("db")
-    ""
-  :proof
-  pignose-parse-db
-  eval-ast)
-
-(defcom  ("clause")
-    ""
-  :proof
-  pignose-parse-clause
-  eval-ast)
-
-(defcom  ("list")
-    ""
-  :proof
-  pignose-parse-list-command
-  eval-ast)
-
-(defcom ("flag")
-    ""
-  :proof
-  pignose-parse-flag
-  eval-ast)
-
-(defcom  ("param")
-    ""
-  :proof
-  pignose-parse-param
-  eval-ast)
-
-(defcom ("option")
-    ""
-  :proof
-  pignose-parse-option
-  eval-ast)
-
-(defcom ("resolve")
-    ""
-  :proof
-  pignose-parse-resolve
-  eval-ast)
-
-(defcom  ("demod")
-    ""
-  :proof
-  pignose-parse-demod
-  eval-ast)
-
-(defcom ("save-option")
-    ""
-  :proof
-  pignose-parse-save-option
-  eval-ast)
-
-(defcom ("sigmatch")
-    ""
-  :proof
-  pignose-parse-sigmatch
-  eval-ast)
-
-(defcom  ("lex")
-    ""
-  :proof
-  pignose-parse-lex
-  eval-ast)
-
-(defcom (".")
-    ""
-  :misc
-  identity
-  cafeobj-nop)
-
-;;; 
-;;; All the Declaration forms --------------------------------------------------------------
-;;;
-
-(defdecl ("bsort")
-    ""
-  :sig
-  process-bsort-declaration
-  eval-ast)
-
-(defdecl ("[")
-    ""
-  :sig
-  process-sort-and-subsort-form
-  eval-ast)
-
-(defdecl ("hidden" "*")
-    ""
-  :sig
-  process-hidden-sort-form
-  eval-ast)
-
-(defdecl ("op")
-    ""
-  :sig 
-  process-operator-declaration-form
-  eval-ast)
-
-(defdecl ("ops")
-  ""
-  :sig 
-  process-operators-declaration-form
-  eval-ast)
-
-(defdecl ("bop")
-    ""
-  :sig process-operator-declaration-form
-  eval-ast)
-
-(defdecl ("bops")
-    ""
-  :sig 
-  process-boperators-declaration-form
-  eval-ast)
-
-(defdecl ("pred")
-    ""
-  :sig
-  process-predicate-declaration-form
-  eval-ast)
-
-(defdecl ("dpred")
-    ""
-  :sig 
-  process-predicate-declaration-form
-  eval-ast)
-              
-(defdecl ("bpred")
-    ""
-  :sig 
-  process-predicate-declaration-form
-  eval-ast)
-              
-(defdecl ("dbpred")
-    ""
-  :sig 
-  process-predicate-declaration-form
-  eval-ast)
-              
-;;;(defdecl ("opattr" "attr" "attrs")
-;;;    ""
-;;;  :sig
-;;;  process-opattr-declaration-form
-;;;  eval-ast)
-              
-(defdecl ("rec" "record")
-    ""
-  :sig 
-  process-record-declaration-form
-  eval-ast)
-
-;;(defdecl ("cls" "class")
-;;    ""
-;;  :sig process-class-declaration-form
-;;  eval-ast)
-
-(defdecl ("let")
-    ""
-  :ax 
-  process-let-declaration-form
-  eval-ast)
-
-(defdecl ("#define")
-    ""
-  :ax
-  process-macro-declaration-form
-  eval-ast)
-
-(defdecl ("eq" "cq" "ceq" "rule" "rl" "crl" "crule" "trans" "ctrans" "trns" "ctrns"
-	       "beq" "bceq" "brule" "brl" "bcrule" "bcrl" "btrans" "btrns"
-	       "bctrans" "bctrns")
-    ""
-  :ax
-  process-axiom-form
-  eval-ast)
-
-(defdecl ("var" "vars")
-    ""
-  :ax
-  process-variable-declaration-form
-  eval-ast)
-              
-(defdecl ("pvar" "pvars")
-    ""
-  :ax
-  process-pseud-variable-declaration-form
-  eval-ast)
-              
-(defdecl ("fax" "bfax" "ax" "bax" "frm" "bfrm")
-    ""
-  :ax
-  pignose-process-fax-proc
-  eval-ast)
-
-(defdecl ("goal" "bgoal")
-    ""
-  :ax
-  pignose-process-goal-proc
-  eval-ast)
-              
-(defdecl ("imports" "import")
-    ""
-  :sig
-  parse-imports-form
-  eval-ast)
-
-(defdecl ("pr" "protecting" "ex" "extending" "us" "using" "inc" "including")
-    ""
-  :sig 
-  process-importation-form
-  eval-ast)
-
-(defdecl ("--" "**")
-    ""
-  :ignore
-  parse-decl-do-nothing
-  eval-decl-do-nothing)
-
-(defdecl ("-->")
-    ""
-  :ignore
-  parse-dynamic-comment-1
-  eval-decl-do-nothing)
-
-(defdecl ("**>")
-    ""
-  :ignore
-  parse-dynamic-comment-2
-  eval-decl-do-nothing)
-
-(defdecl ("ev" "lisp" "evq" "lispq")
-    ""
-  :ignore
-  process-ev-lisp-form
-  eval-decl-do-nothing)
-
-(defdecl ("eval")
-    ""
-  :misc
-  parse-eval-form
-  eval-ast)
-
-(defdecl ("sig" "signature")
-    ""
-  :sig
-  process-signature
-  eval-ast)
-
-(defdecl ("axioms" "axiom" "axs")
-    ""
-  :ax 
-  process-axioms-declaration
-  eval-ast)
-
-(defdecl (".")                    ; sole dots
-    ""
-  :ignore
-  parse-decl-do-nothing
-  eval-decl-do-nothing)
-
-
-)
diff --git a/cafeobj/define.lisp b/cafeobj/define.lisp
new file mode 100644
index 0000000..cc431ea
--- /dev/null
+++ b/cafeobj/define.lisp
@@ -0,0 +1,199 @@
+;;;-*- Mode:LISP; Package:CHAOS; Base:10; Syntax:Common-lisp -*-
+#|==============================================================================
+                            System: CHAOS
+                           Module: cafeobj
+                          File: define.lisp
+==============================================================================|#
+(in-package :chaos)
+#-:chaos-debug
+(declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
+#+:chaos-debug
+(declaim (optimize (speed 1) (safety 3) #-GCL (debug 3)))
+
+
+;;; *****************************************************
+;;; On line document for commands, declarations or others 
+;;; *****************************************************
+
+(defvar *cafeobj-doc-db* (make-hash-table :test #'equal))
+
+(defstruct (oldoc (:print-function print-online-document))
+  (key        ""  :type string)		; 
+  (doc-string ""  :type string)		; document string of commad/declaration
+  (names      nil :type list)		;
+  )
+
+(defun print-online-document (doc &optional (stream *standard-output*) &rest ignore)
+  (declare (ignore ignore))
+  (format stream "~%*** key    : ~a" (oldoc-key doc))
+  (format stream "~&doc-string : ~a" (oldoc-doc-string doc))
+  (format stream "~&name       : ~a" (oldoc-names doc)))
+
+(defun get-document-string (key)
+  (let ((doc (gethash key *cafeobj-doc-db*)))
+    (if doc
+	(oldoc-doc-string doc)
+      nil)))
+
+(defun show-doc-entries ()
+  (let ((keys nil))
+    (maphash #'(lambda (k v) (declare (ignore v)) (push k keys)) *cafeobj-doc-db*)
+    (setq keys (sort keys #'string<=))
+    (dolist (key keys)
+      (let ((oldoc (get-document-string key)))
+	(format t "~s" oldoc)))))
+
+;;;
+;;; register-online-help : names doc 
+;;;
+
+(defun make-doc-key-from-string (str)
+  (when (atom str)
+    (setq str (list str)))
+  (let ((keys nil))
+    (dolist (s str)
+      (let ((keyl (remove "" (parse-with-delimiter s #\space))))
+	(push (reduce #'(lambda (x y) (concatenate 'string x y)) keyl) keys)))
+    keys))
+
+(defun register-online-help (names doc)
+  (unless doc (return-from register-online-help nil))
+  (cond ((stringp doc)
+	 (dolist (name names)
+	   (dolist (key (make-doc-key-from-string name))
+	     (setf (gethash key *cafeobj-doc-db*) (make-oldoc :key key
+							      :doc-string doc
+							      :names name)))))
+	(t (dolist (a-doc doc)
+	     (let ((key-parts (butlast a-doc))
+		   (doc-string (car (last a-doc))))
+	       (dolist (keyp key-parts)
+		 (dolist (key (make-doc-key-from-string keyp))
+		   (setf (gethash key *cafeobj-doc-db*) (make-oldoc :key key
+								    :doc-string doc-string
+								    :names keyp)))))))))
+
+(defparameter .md-special-chars.
+    '((#\# #\null)
+      (#\` #\')
+      (#\~ #\null)))
+
+(defun format-description (doc)
+  (parallel-substitute .md-special-chars. doc))
+;;; ******
+;;; DEFINE : define command or declaration
+;;; ******
+
+(defvar *cafeobj-top-commands* (make-hash-table :test #'equal))
+(defvar *cafeobj-declarations* (make-hash-table :test #'equal))
+
+(defstruct (comde (:print-function print-comde))
+  (key       ""  :type string)		; command/declaration keyword
+  (type      nil :type symbol)		; command or declaration
+  (category  nil :type symbol)		; kind of command/declaration
+  (parser    nil :type symbol)		; parser function
+  (evaluator nil :type symbol)		; evaluator function
+  )
+
+(defparameter .valid-comde-types. '(:top :inner-module :doc-only))
+(defparameter .valid-decl-categories. 
+    '(:decl-toplevel			; toplevel declaration, such as 'module', 'view', e.t.c.
+					; i.e., declarations which can apper at toplevel.
+      :signature			; signature part of module body, such as 'op' '[', e.t.c
+      :axiom				; axiom part of mdoule body, such as 'eq, ceq', e.t.c
+      :ignore				; comments, dot (.), lisp, ev, e.t.c.
+      :import				; import part of module body, such as 'protecting'
+      :misc
+      ))
+
+(defparameter .valid-com-categories.
+    '(:decl-toplevel	       ; toplevel declaration, such as 'module', 'view', e.t.c.
+      :checker		       ; check command
+      :module		       ; apply some modifications to a module, such as regularize
+      :rewrite		       ; commands related to rewriting, such as 'reduce', 'execute', e.t.c.
+      :parse		       ; commands related to parsing terms, such as 'parse', e.t.c
+      :inspect		       ; commands inspecting modules, terms, such as 'show', 'match', e.t.c
+      :module-element	       ; declarations which can apper when a module is open.
+      :proof		       ; commands related to proof stuff, such as 'open', 'apply, e.t.c.
+      :switch		       ; 'set' commands
+      :system		       ; various system related commands, such as 'protect', 'reset', e.t.c.
+      :library		       ; library related commands, such as 'autoload', 'provide', e.t.c.
+      :help		       ; '?', '??' 
+      :io		       ; 'input', 'save', e.t.c.
+      :misc		       ; 
+      ))
+
+(defun print-comde (me &optional (stream *standard-output*) &rest ignore)
+  (declare (ignore ignore))
+  (format stream "~%** key         : ~a" (comde-key me))
+  (format stream "~%   type        : ~a" (comde-type me))
+  (format stream "~%   category    : ~a" (comde-category me))
+  (format stream "~%   parser      : ~a" (comde-parser me))
+  (format stream "~%   evaluator   : ~a" (comde-evaluator me)))
+
+;;;
+;;; get-command-info
+;;;
+(defun get-command-info (key)
+  (gethash key *cafeobj-top-commands*))
+
+
+(defun show-top-entries ()
+  (let ((keys nil))
+    (maphash #'(lambda (k v) (declare (ignore v)) (push k keys)) *cafeobj-top-commands*)
+    (setq keys (sort keys #'string<=))
+    (dolist (key keys)
+      (format t "~s" (get-command-info key)))))
+
+;;;
+;;; get-decl-info
+;;;
+(defun get-decl-info (key)
+  (gethash key *cafeobj-declarations*))
+
+(defun show-decl-entries ()
+  (let ((keys nil))
+    (maphash #'(lambda (k v) (declare (ignore v)) (push k keys)) *cafeobj-declarations*)
+    (setq keys (sort keys #'string<=))
+    (dolist (key keys)
+      (format t "~s" (get-decl-info key)))))
+
+;;;
+;;; DEFINE
+;;; 
+(defmacro define ((&rest keys) &key (type :top)
+				    (category :misc)
+				    (parser nil)
+				    (evaluator 'eval-ast)
+				    (doc nil))
+    (case type
+      (:top (unless (member category .valid-com-categories.)
+	      (error "Internal error, invalid category ~s" category)))
+      (:inner-module (unless (member category .valid-decl-categories.)
+			(error "Internal error, invalid category ~s" category)))
+      (:doc-only)
+      (:otherwise (error "Internal error, invalid type ~s" type)))
+    (unless (eq type :doc-only)
+      (unless (fboundp parser) (warn "no parser ~s" parser))
+      (unless (fboundp evaluator) (warn "no evaluator ~s" evaluator)))
+    ;;
+    `(progn
+       (unless (eq ,type :doc-only)
+	 (let ((hash (if (or (eq ,type :top)
+			     (eq ,category :decl-toplevel))
+			 *cafeobj-top-commands*
+		       *cafeobj-declarations*)))
+	   (dolist (key ',keys)
+	     (setf (gethash key hash) (make-comde :key key
+						  :type ',type
+						  :category ',category
+						  :parser ',parser
+						  :evaluator ',evaluator)))))
+       ;; set online help
+       (register-online-help ',keys ',doc)))
+
+(defun print-comde-usage (com)
+  (format t "~&[Usage] ~s, not yet" com))
+
+
+;;; EOF
diff --git a/cafeobj/trans-decl.lisp b/cafeobj/trans-decl.lisp
index 0091eae..d8852bd 100644
--- a/cafeobj/trans-decl.lisp
+++ b/cafeobj/trans-decl.lisp
@@ -25,8 +25,6 @@
 ;;; parser were more well done, the translators would be no more needed, or
 ;;; would be more clean. This should be done in the near future.
 ;;; ****************************************************************************
-
-(defvar *cafeobj-declarations* (make-hash-table :test #'equal))
 
 ;;; ***************
 ;;; INTERFACE  FORM____________________________________________________________
@@ -770,18 +768,19 @@
 	  (parse-module-element e)
 	(case kind
 	  ((:ignore :misc) nil)
-	  (:sig (setq sig (nconc sig elt)))
-	  (:ax (setq ax (nconc ax elt))))))
+	  (:signature (setq sig (nconc sig elt)))
+	  (:import (setq sig (nconc sig elt)))
+	  (:axiom (setq ax (nconc ax elt))))))
     (setf body (append sig ax))
     body))
 
 (defun parse-module-element (e &rest ignore)
   (declare (ignore ignore))
-  (let ((decl (gethash (car e) *cafeobj-declarations*)))
+  (let ((decl (get-decl-info (car e))))
     (unless decl
       (with-output-chaos-error ('no-decl)
 	(format t "No such declaration '~a'" (car e))))
-    (let ((parser (decl-parser decl)))
+    (let ((parser (comde-parser decl)))
       (unless parser
 	(with-output-chaos-error ('no-parser)
 	  (format t "No parser is defined for declaration ~a" (car e))))
@@ -789,7 +788,7 @@
 	(declare (list ast))
 	(when (and ast (atom (car ast)))
 	  (setq ast (list ast)))
-	(values (decl-category decl) ast)))))
+	(values (comde-category decl) ast)))))
 
 (defun parse-module-element-1 (e &rest ignore)
   (multiple-value-bind (type elt)
diff --git a/chaos/tools/help.lisp b/chaos/tools/help.lisp
index 9bf6ce6..dc67319 100644
--- a/chaos/tools/help.lisp
+++ b/chaos/tools/help.lisp
@@ -2,8 +2,8 @@
 (in-package :chaos)
 #|==============================================================================
                             System: CHAOS
-				          Module: chaos/tools
-			              File: help.lisp
+		          Module: chaos/tools
+                            File: help.lisp
 ==============================================================================|#
 #-:chaos-debug
 (declaim (optimize (speed 3) (safety 0) #-GCL (debug 0)))
diff --git a/cl-ppcre b/cl-ppcre
new file mode 160000
index 0000000..df1590a
--- /dev/null
+++ b/cl-ppcre
@@ -0,0 +1 @@
+Subproject commit df1590a21f378e97512dd8fec0373f011115530d
diff --git a/configure b/configure
index ef26796..b01191e 100755
--- a/configure
+++ b/configure
@@ -1695,7 +1695,7 @@
 VERSION=1.4
 VMINOR=.13
 VMEMO=PigNose0.99
-PATCHLEVEL=p7
+PATCHLEVEL=p9
 
 
 
diff --git a/configure.in b/configure.in
index 4529104..b5cfbae 100644
--- a/configure.in
+++ b/configure.in
@@ -8,7 +8,7 @@
 VERSION=1.4
 VMINOR=.13
 VMEMO=PigNose0.99
-PATCHLEVEL=p7
+PATCHLEVEL=p9
 AC_SUBST(PACKAGE)
 AC_SUBST(VERSION)
 AC_SUBST(VMINOR)
diff --git a/make-cafeobj.lisp b/make-cafeobj.lisp
index 54979d0..6ddac62 100644
--- a/make-cafeobj.lisp
+++ b/make-cafeobj.lisp
@@ -192,6 +192,8 @@
   ;; (mk::operate-on-system :chaosx :compile)
   (setq chaos::*compile-builtin-axiom* nil)
   (load "sysdef.asd")
+  (load "cl-ppcre/cl-ppcre.asd")
+  (asdf:oos 'asdf:load-op :cl-ppcre)
   (asdf:oos 'asdf:load-op 'chaosx)
   (make-exec-image
    (concatenate 'string *chaos-root*
diff --git a/sysdef.asd b/sysdef.asd
index 8109b5c..76a8c3f 100644
--- a/sysdef.asd
+++ b/sysdef.asd
@@ -189,12 +189,14 @@
 	      :serial t
 	      :components ((:file "cafeobjvar")
 			   (:file "creader")
+			   (:file "define")
 			   (:file "trans-com")
 			   (:file "trans-decl")
 			   (:file "trans-form")
 			   ;; (:file "command-proc")
 			   (:file "command-top")
-			   (:file "defcommand")
+			   (:file "commands")
+			   (:file "declarations")
 			   (:file "cafeobj-top")
 			   ))
 
diff --git a/sysdef.cl b/sysdef.cl
index 3abeadf..48aa7ba 100644
--- a/sysdef.cl
+++ b/sysdef.cl
@@ -194,11 +194,13 @@
                             "cafeobj/cafeobjvar"
                             (:serial
                              "cafeobj/creader"
+			     "cafeobj/define"
                              "cafeobj/trans-com"
                              "cafeobj/trans-decl"
                              ;; "cafeobj/command-proc"
                              "cafeobj/command-top"
-			     "cafeobj/defcommand"
+			     "cafeobj/commands"
+			     "cafeobj/declarations"
                              "cafeobj/cafeobj-top")))
          
          "acl-init"
diff --git a/version.lisp b/version.lisp
index f1c9c1c..7770fe9 100644
--- a/version.lisp
+++ b/version.lisp
@@ -9,7 +9,7 @@
 (eval-when (:execute :load-toplevel :compile-toplevel)
   (setq cafeobj-version-major "1.4")
   (setq cafeobj-version-memo (format nil "~a" "PigNose0.99"))
-  (setq patch-level (format nil "~a" "p7"))
+  (setq patch-level (format nil "~a" "p9"))
   (if (not (equal "" cafeobj-version-memo))
       (if (not (equal "" patch-level))
           (setq cafeobj-version-minor