src/Pure/ML/ml_antiquote.ML
changeset 37868 59eed00bfd8e
parent 37304 645f849eefa7
child 40110 93e7935d4cb5
equal deleted inserted replaced
37867:b9783e9e96e1 37868:59eed00bfd8e
    62 val _ = value "binding"
    62 val _ = value "binding"
    63   (Scan.lift (Parse.position Args.name)
    63   (Scan.lift (Parse.position Args.name)
    64     >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
    64     >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
    65 
    65 
    66 val _ = value "theory"
    66 val _ = value "theory"
    67   (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
    67   (Scan.lift Args.name >> (fn name =>
       
    68     "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
    68   || Scan.succeed "ML_Context.the_global_context ()");
    69   || Scan.succeed "ML_Context.the_global_context ()");
    69 
    70 
    70 val _ = value "theory_ref"
    71 val _ = value "theory_ref"
    71   (Scan.lift Args.name >> (fn name =>
    72   (Scan.lift Args.name >> (fn name =>
    72     "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
    73     "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
       
    74       ML_Syntax.print_string name ^ ")")
    73   || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
    75   || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
    74 
    76 
    75 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
    77 val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
    76 
    78 
    77 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
    79 val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));