proper PIDE markup for codegen arguments;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Jul 30 21:22:37 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Jul 30 22:31:34 2013 +0200
@@ -272,7 +272,7 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
     "prove equations for predicate specified by intro/elim rules"
-    (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
+    (opt_expected_modes -- opt_modes -- scan_options -- Parse.term >> code_pred_cmd)
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "values"}

--- a/src/Tools/Code/code_haskell.ML	Tue Jul 30 21:22:37 2013 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jul 30 22:31:34 2013 +0200
@@ -463,19 +463,21 @@
 fun add_monad target' raw_c_bind thy =
   let
     val c_bind = Code.read_const thy raw_c_bind;
-  in if target = target' then
-    thy
-    |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
-      SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
-  else error "Only Haskell target allows for monad syntax" end;
+  in
+    if target = target' then
+      thy
+      |> Code_Target.set_printings (Code_Symbol.Constant (c_bind, [(target,
+        SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind)))]))
+    else error "Only Haskell target allows for monad syntax"
+  end;
 
 
 (** Isar setup **)
 
 val _ =
   Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
-    (Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
-      Toplevel.theory  (add_monad target raw_bind)));
+    (Parse.term -- Parse.name >> (fn (raw_bind, target) =>
+      Toplevel.theory (add_monad target raw_bind)));
 
 val setup =
   Code_Target.add_target

--- a/src/Tools/Code/code_target.ML	Tue Jul 30 21:22:37 2013 +0200
+++ b/src/Tools/Code/code_target.ML	Tue Jul 30 22:31:34 2013 +0200
@@ -752,7 +752,7 @@
     -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target)));
 
 fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module =
-  parse_single_symbol_pragma @{keyword "constant"} Parse.term_group parse_const
+  parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const
     >> Code_Symbol.Constant
   || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco
     >> Code_Symbol.Type_Constructor
@@ -784,7 +784,7 @@
     -- code_expr_argsP)))
       >> (fn seri_args => check_code_cmd raw_cs seri_args);
 
-val code_exprP = Scan.repeat1 Parse.term_group
+val code_exprP = Scan.repeat1 Parse.term
   :|-- (fn raw_cs => (code_expr_checkingP raw_cs || code_expr_inP raw_cs));
 
 val _ =
@@ -812,7 +812,7 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
-    (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+    (process_multi_syntax Parse.term Code_Printer.parse_const_syntax
       add_const_syntax_cmd);
 
 val _ =
@@ -842,7 +842,7 @@
 val _ =
   Outer_Syntax.command @{command_spec "code_abort"}
     "permit constant to be implemented as program abort"
-    (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd));
+    (Scan.repeat1 Parse.term >> (Toplevel.theory o fold allow_abort_cmd));
 
 val _ =
   Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"

--- a/src/Tools/Code/code_thingol.ML	Tue Jul 30 21:22:37 2013 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jul 30 22:31:34 2013 +0200
@@ -1018,10 +1018,16 @@
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
-    fun read_const_expr "_" = ([], consts_of thy)
-      | read_const_expr s = if String.isSuffix "._" s
+
+    val ctxt = Proof_Context.init_global thy;
+    fun read_const_expr str =
+      (case Syntax.parse_token ctxt (K NONE) Markup.empty (SOME o Symbol_Pos.implode o #1) str of
+        SOME "_" => ([], consts_of thy)
+      | SOME s =>
+          if String.isSuffix "._" s
           then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
-          else ([Code.read_const thy s], []);
+          else ([Code.read_const thy str], [])
+      | NONE => ([Code.read_const thy str], []));
   in pairself flat o split_list o map read_const_expr end;
 
 fun code_depgr thy consts =
@@ -1061,14 +1067,14 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_thms"}
     "print system of code equations for code"
-    (Scan.repeat1 Parse.term_group >> (fn cs =>
+    (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.unknown_theory o
       Toplevel.keep (fn state => code_thms_cmd (Toplevel.theory_of state) cs)));
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "code_deps"}
     "visualize dependencies of code equations for code"
-    (Scan.repeat1 Parse.term_group >> (fn cs =>
+    (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.unknown_theory o
       Toplevel.keep (fn state => code_deps_cmd (Toplevel.theory_of state) cs)));