src/Pure/Thy/thy_info.ML
changeset 24696 b5e68fe31eba
parent 24563 f2edc70f8962
child 25013 bf4f7571407f
equal deleted inserted replaced
24695:2892482a4e62 24696:b5e68fe31eba
   205 val _ = ML_Context.value_antiq "theory"
   205 val _ = ML_Context.value_antiq "theory"
   206   (Scan.lift Args.name
   206   (Scan.lift Args.name
   207     >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
   207     >> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name))
   208   || Scan.succeed ("thy", "ML_Context.the_context ()"));
   208   || Scan.succeed ("thy", "ML_Context.the_context ()"));
   209 
   209 
       
   210 val _ = ML_Context.value_antiq "theory_ref"
       
   211   (Scan.lift Args.name
       
   212     >> (fn name => (name ^ "_thy",
       
   213         "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")"))
       
   214   || Scan.succeed ("thy", "Theory.check_thy (ML_Context.the_context ())"));
       
   215 
   210 
   216 
   211 
   217 
   212 (** thy operations **)
   218 (** thy operations **)
   213 
   219 
   214 (* check state *)
   220 (* check state *)