comparison src/compiler.sml @ 1815:28986cfac833

Added 'coreInline' and 'monoInline' .urp options
author Vladimir Shabanov <vshabanoff@gmail.com>
date Tue, 04 Sep 2012 03:32:59 +0400
parents 38297294cf98
children 8bc16ff91d32
comparison
equal deleted inserted replaced
1814:2d9f831d45c9 1815:28986cfac833
851 | _ => ErrorMsg.error "invalid 'limit' arguments") 851 | _ => ErrorMsg.error "invalid 'limit' arguments")
852 | "minHeap" => 852 | "minHeap" =>
853 (case Int.fromString arg of 853 (case Int.fromString arg of
854 NONE => ErrorMsg.error ("invalid min heap '" ^ arg ^ "'") 854 NONE => ErrorMsg.error ("invalid min heap '" ^ arg ^ "'")
855 | SOME n => minHeap := n) 855 | SOME n => minHeap := n)
856 | "coreInline" =>
857 (case Int.fromString arg of
858 NONE => ErrorMsg.error ("invalid core inline level '" ^ arg ^ "'")
859 | SOME n => Settings.setCoreInline n)
860 | "monoInline" =>
861 (case Int.fromString arg of
862 NONE => ErrorMsg.error ("invalid mono inline level '" ^ arg ^ "'")
863 | SOME n => Settings.setMonoInline n)
856 | "alwaysInline" => Settings.addAlwaysInline arg 864 | "alwaysInline" => Settings.addAlwaysInline arg
857 | "noXsrfProtection" => Settings.addNoXsrfProtection arg 865 | "noXsrfProtection" => Settings.addNoXsrfProtection arg
858 | "timeFormat" => Settings.setTimeFormat arg 866 | "timeFormat" => Settings.setTimeFormat arg
859 867
860 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'"); 868 | _ => ErrorMsg.error ("Unrecognized command '" ^ cmd ^ "'");