globbing constant expressions use more idiomatic underscore rather than star
authorhaftmann
Fri Nov 26 12:03:18 2010 +0100 (2010-11-26)
changeset 4071181bc73585eec
parent 40710 499aa989fbad
child 40712 ed0add6f69a7
globbing constant expressions use more idiomatic underscore rather than star
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/Codegenerator_Test/Generate_Pretty.thy
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 12:03:17 2010 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Fri Nov 26 12:03:18 2010 +0100
     1.3 @@ -1082,7 +1082,7 @@
     1.4      const: term
     1.5      ;
     1.6  
     1.7 -    constexpr: ( const | 'name.*' | '*' )
     1.8 +    constexpr: ( const | 'name._' | '_' )
     1.9      ;
    1.10  
    1.11      typeconstructor: nameref
    1.12 @@ -1144,7 +1144,7 @@
    1.13      ;
    1.14  
    1.15      'code_reflect' string \\
    1.16 -      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.17 +      ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
    1.18        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    1.19      ;
    1.20  
     2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 12:03:17 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Nov 26 12:03:18 2010 +0100
     2.3 @@ -1098,7 +1098,7 @@
     2.4      const: term
     2.5      ;
     2.6  
     2.7 -    constexpr: ( const | 'name.*' | '*' )
     2.8 +    constexpr: ( const | 'name._' | '_' )
     2.9      ;
    2.10  
    2.11      typeconstructor: nameref
    2.12 @@ -1160,7 +1160,7 @@
    2.13      ;
    2.14  
    2.15      'code_reflect' string \\
    2.16 -      ( 'datatypes' ( string '=' ( '"*"' | ( string + '|' ) + 'and' ) ) ) ? \\
    2.17 +      ( 'datatypes' ( string '=' ( '_' | ( string + '|' ) + 'and' ) ) ) ? \\
    2.18        ( 'functions' ( string + ) ) ? ( 'file' string ) ?
    2.19      ;
    2.20  
     3.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Nov 26 12:03:17 2010 +0100
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Nov 26 12:03:18 2010 +0100
     3.3 @@ -14,6 +14,6 @@
     3.4    by a corresponding @{text export_code} command.
     3.5  *}
     3.6  
     3.7 -export_code "*" checking SML OCaml? Haskell? Scala?
     3.8 +export_code _ checking SML OCaml? Haskell? Scala?
     3.9  
    3.10  end
     4.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Nov 26 12:03:17 2010 +0100
     4.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Nov 26 12:03:18 2010 +0100
     4.3 @@ -19,6 +19,6 @@
     4.4    by a corresponding @{text export_code} command.
     4.5  *}
     4.6  
     4.7 -export_code "*" checking SML OCaml? Haskell? Scala?
     4.8 +export_code _ checking SML OCaml? Haskell? Scala?
     4.9  
    4.10  end
     5.1 --- a/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:17 2010 +0100
     5.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Nov 26 12:03:18 2010 +0100
     5.3 @@ -349,7 +349,8 @@
     5.4  val _ = List.app Keyword.keyword [datatypesK, functionsK];
     5.5  
     5.6  val parse_datatype =
     5.7 -  Parse.name --| Parse.$$$ "=" -- ((Parse.string >> (fn "*" => NONE | _ => Scan.fail ()))
     5.8 +  Parse.name --| Parse.$$$ "=" --
     5.9 +    (((Parse.sym_ident || Parse.string) >> (fn "_" => NONE | _ => Scan.fail ()))
    5.10      || ((Parse.term ::: (Scan.repeat (Parse.$$$ "|" |-- Parse.term))) >> SOME));
    5.11  
    5.12  in
     6.1 --- a/src/Tools/Code/code_thingol.ML	Fri Nov 26 12:03:17 2010 +0100
     6.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Nov 26 12:03:18 2010 +0100
     6.3 @@ -940,9 +940,9 @@
     6.4      fun belongs_here thy' c = forall
     6.5        (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     6.6      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     6.7 -    fun read_const_expr "*" = ([], consts_of thy)
     6.8 -      | read_const_expr s = if String.isSuffix ".*" s
     6.9 -          then ([], consts_of_select (Context.this_theory thy (unsuffix ".*" s)))
    6.10 +    fun read_const_expr "_" = ([], consts_of thy)
    6.11 +      | read_const_expr s = if String.isSuffix "._" s
    6.12 +          then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s)))
    6.13            else ([Code.read_const thy s], []);
    6.14    in pairself flat o split_list o map read_const_expr end;
    6.15