/[mojave]/metaprl/theories/tactic/mptop.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/mptop.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3086 by nogin, Sun Oct 22 20:58:58 2000 UTC revision 3278 by nogin, Wed Jun 20 00:27:36 2001 UTC
# Line 156  Line 156 
156  type top_table =  type top_table =
157     (string, string * expr) Hashtbl.t     (string, string * expr) Hashtbl.t
158    
 (*!  
  * @begin[doc]  
  * Toplevel values are added to the @Comment!resource[toploop_resource] resource.  
  * The argument has type @code{string * expr}, which includes  
  * the string name of the value, and it's value.  
  * @docoff  
  * @end[doc]  
  *)  
 resource (string * expr, top_table, top_data, unit) toploop_resource  
   
159  (************************************************************************  (************************************************************************
160   * IMPLEMENTATION                                                       *   * IMPLEMENTATION                                                       *
161   ************************************************************************)   ************************************************************************)
# Line 729  Line 719 
719   | [] ->   | [] ->
720        base        base
721    
722  let toploop_resource =  (*!
723     Mp_resource.create (**)   * @begin[doc]
724        { resource_join = join_resource;   * Toplevel values are added to the @Comment!resource[toploop_resource] resource.
725          resource_extract = extract_resource;   * The argument has type @code{string * expr}, which includes
726          resource_improve = improve_resource;   * the string name of the value, and it's value.
727          resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";   * @docoff
728          resource_close = close_resource   * @end[doc]
729        }   *)
730        (add_resources Empty values)  let resource toploop = {
731       resource_empty = add_resources Empty values;
732       resource_join = join_resource;
733       resource_extract = extract_resource;
734       resource_improve = improve_resource;
735       resource_improve_arg = Mp_resource.improve_arg_fail "toploop_resource";
736       resource_close = close_resource
737    }
738    
739  let get_resource modname =  let get_resource modname =
740     Mp_resource.find toploop_resource modname     Mp_resource.find toploop_resource modname

Legend:
Removed from v.3086  
changed lines
  Added in v.3278

  ViewVC Help
Powered by ViewVC 1.1.26