Structure parse_term

signature parse_term =
sig
  type 'a PStack
  type 'a qbuf = 'a qbuf.qbuf
  type term = Term.term
  datatype stack_terminal = datatype parse_term_dtype.stack_terminal
  val STtoString : term_grammar.grammar -> stack_terminal -> string

  val initial_pstack : 'a PStack
  val is_final_pstack : 'a PStack -> bool
  val top_nonterminal : term PStack -> Absyn.absyn

  exception PrecConflict of stack_terminal * stack_terminal
  exception ParseTermError of string locn.located

  val parse_term :
      term_grammar.grammar ->
      (term qbuf -> Pretype.pretype) ->
      (term qbuf * term PStack, unit, string locn.located) errormonad.t

  datatype mx_order = datatype parse_term_dtype.mx_order
  type 'a stbstab  (* abstract; backed by a local Table instantiation
                      keyed on (stack_terminal * bool) * stack_terminal --
                      not exposed as a structure to avoid leaking the
                      TABLE signature, which trips mosml on
                      case-insensitive filesystems *)
  val mk_prec_matrix :
      term_grammar.grammar -> mx_order stbstab Uref.t

end

HOL 4, Trindemossen-2