Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
OuterSyntax.scan: pass position;
authorwenzelm
Tue, 12 Aug 2008 21:28:09 +0200
changeset 27845 141772c866c9
parent 27844 86f0f91471d0
child 27846 2828a276dc93
OuterSyntax.scan: pass position;
src/Tools/code/code_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Tools/code/code_target.ML	Tue Aug 12 21:28:07 2008 +0200
+++ b/src/Tools/code/code_target.ML	Tue Aug 12 21:28:09 2008 +0200
@@ -2315,7 +2315,8 @@
     K.diag (P.!!! (code_exprP export_code_cmd) >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
 fun shell_command thyname cmd = Toplevel.program (fn _ =>
-  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd)) ((filter OuterLex.is_proper o OuterSyntax.scan) cmd)
+  (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! (code_exprP export_code_cmd))
+    ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd)
    of SOME f => (writeln "Now generating code..."; f (theory thyname))
     | NONE => error ("Bad directive " ^ quote cmd)))
   handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
isabelle