ProgTutorial/antiquote_setup.ML
changeset 317 d69214e47ef9
parent 316 74f0a06f751f
child 328 c0cae24b9d46
equal deleted inserted replaced
316:74f0a06f751f 317:d69214e47ef9
    85 fun ouput_response_fake_both _ (lhs, pat) = 
    85 fun ouput_response_fake_both _ (lhs, pat) = 
    86     output ((split_lines lhs) @ (prefix_lines "> " pat))
    86     output ((split_lines lhs) @ (prefix_lines "> " pat))
    87 
    87 
    88 val single_arg = Scan.lift (Args.name)
    88 val single_arg = Scan.lift (Args.name)
    89 val two_args   = Scan.lift (Args.name -- Args.name)
    89 val two_args   = Scan.lift (Args.name -- Args.name)
       
    90 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
    90 
    91 
    91 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
    92 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
    92 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
    93 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
    93 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
    94 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
    94 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind
    95 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind
    96 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
    97 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
    97 val _ = ThyOutput.antiquotation "ML_response" two_args output_response
    98 val _ = ThyOutput.antiquotation "ML_response" two_args output_response
    98 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
    99 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
    99 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
   100 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
   100 
   101 
       
   102 (* FIXME: experimental *)
       
   103 fun ml_eq (lhs, pat, eq) =
       
   104   implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] 
       
   105 
       
   106 fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = 
       
   107     (case eq of 
       
   108        NONE => eval_fn ctxt (ml_pat (lhs, pat))
       
   109      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
       
   110      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
       
   111 
       
   112 val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq
       
   113 
       
   114 (* checks whether a file exists in the Isabelle distribution *)
   101 fun href_link txt =
   115 fun href_link txt =
   102 let 
   116 let 
   103   val raw = Symbol.encode_raw
   117   val raw = Symbol.encode_raw
   104   val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
   118   val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
   105 in
   119 in
   106  implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
   120  implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
   107 end 
   121 end 
   108 
   122 
   109 (* checks whether a file exists in the Isabelle distribution *)
       
   110 fun check_file_exists _ txt =
   123 fun check_file_exists _ txt =
   111   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
   124   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
   112    then output [href_link txt]
   125    then output [href_link txt]
   113    else error (implode ["Source file ", quote txt, " does not exist."]))
   126    else error (implode ["Source file ", quote txt, " does not exist."]))
   114 
       
   115 
   127 
   116 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
   128 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
   117 
   129 
   118 
   130 
   119 (* replaces the official subgoal antiquotation with one *)
   131 (* replaces the official subgoal antiquotation with one *)