[isabelle] Isar parser for constant names



Hi,

I'm defining a new Isar-command (called hipster) which should take a list of constant names as input. However, I seem to run into some problems. The parser I’ve written so far works fine, but requires me to pass the arguments as strings, which is somewhat ugly, like this:

hipster "TreeDemo.mirror" "TreeDemo.tmap"

It would be nice to be able to use similar syntax to generate_code, i.e. have the theory names deduced automatically, so I though I’d make use of the function Parse.const. However, although this function parses the constant name to a string, it appears it is not the same one as passing the function names explicitly as a string, which I would expect. 
Checking what Parse.const does with print statements makes me no wiser, here it looks OK. 

Hipster uses the code generator, and this is where the problem manifests itself, when I use Parse.const instead of Parse.string: 

exception TYPE raised (line 97 of "consts.ML"): Unknown constant: "TreeDemo.mirror"

despite being in the theory “TreeDemo”, where indeed there is a function mirror. Below is the code for my small parser, if anyone has any tips on some other function I can use to reliably parse constants names, please let me know! 

Best,
Moa


let
fun call_hipster consts = 
  Local_Theory.target 
  (fn ctxt => fst(Hipster_Explore.explore ctxt consts));
in
Outer_Syntax.local_theory  @{command_spec "hipster"} 
      "Theory Exploration with Hipster”
     (* This works OK*)
      (* (Scan.repeat1 Parse.string >> call_hipster) *)
     (* This cause an error - unknown constant *)
       (Scan.repeat1 Parse.const >> call_hipster)
end



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.