# HG changeset patch
# User wenzelm
# Date 1547401226 -3600
# Node ID e4e5bc6ac21471587391c38ccdd4d0b7672dc61d
# Parent  f044766cd94f47ea5829a6d26d4496629e4e0d5f
tuned;

diff -r f044766cd94f -r e4e5bc6ac214 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sun Jan 13 16:57:25 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Sun Jan 13 18:40:26 2019 +0100
@@ -689,22 +689,21 @@
 
 val code_expr_argsP = Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.args --| \<^keyword>\<open>)\<close>) [];
 
-fun code_expr_inP all_public raw_cs =
+fun code_expr_inP (all_public, raw_cs) =
   Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name
     -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""
     -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.position Parse.path)
     -- code_expr_argsP))
       >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
 
-fun code_expr_checkingP all_public raw_cs =
+fun code_expr_checkingP (all_public, raw_cs) =
   (\<^keyword>\<open>checking\<close> |-- Parse.!!!
-    (Scan.repeat (Parse.name -- ((\<^keyword>\<open>?\<close> |-- Scan.succeed false) || Scan.succeed true)
-    -- code_expr_argsP)))
+    (Scan.repeat (Parse.name -- (Scan.optional (\<^keyword>\<open>?\<close> >> K false) true) -- code_expr_argsP)))
       >> (fn seri_args => check_code_cmd all_public raw_cs seri_args);
 
-val code_exprP = (Scan.optional (\<^keyword>\<open>open\<close> |-- Scan.succeed true) false
-  -- Scan.repeat1 Parse.term)
-  :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs));
+val code_exprP =
+  (Scan.optional (\<^keyword>\<open>open\<close> >> K true) false -- Scan.repeat1 Parse.term)
+    :|-- (fn args => (code_expr_checkingP args || code_expr_inP args));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_reserved\<close>
diff -r f044766cd94f -r e4e5bc6ac214 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Jan 13 16:57:25 2019 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sun Jan 13 18:40:26 2019 +0100
@@ -957,9 +957,9 @@
       (case Syntax.parse_input ctxt (K NONE) (K 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 (this_theory (unsuffix "._" s)))
-          else ([Code.read_const thy str], [])
+          (case try (unsuffix "._") s of
+            SOME name => ([], consts_of_select (this_theory name))
+          | NONE => ([Code.read_const thy str], []))
       | NONE => ([Code.read_const thy str], []));
   in apply2 flat o split_list o map read_const_expr end;