clarified option type;
authorwenzelm
Mon, 07 Oct 2019 21:51:31 +0200
changeset 70801 5352449209b1
parent 70800 44eeca528557
child 70802 160eaf566bcb
child 70806 f2dd07a5459a
clarified option type;
etc/options
src/Pure/PIDE/headless.scala
--- a/etc/options	Mon Oct 07 17:20:26 2019 +0200
+++ b/etc/options	Mon Oct 07 21:51:31 2019 +0200
@@ -222,7 +222,7 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
-option headless_load_limit : int = 5
+option headless_load_limit : real = 5.0
   -- "limit in MB for loaded theory files (0 = unlimited)"
 
 
--- a/src/Pure/PIDE/headless.scala	Mon Oct 07 17:20:26 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Mon Oct 07 21:51:31 2019 +0200
@@ -271,7 +271,7 @@
             maximals.sortBy(node => - depth(node))
           }
         val load_limit =
-          if (commit.isDefined) session_options.int("headless_load_limit").toLong * 1024 * 1024
+          if (commit.isDefined) (session_options.real("headless_load_limit") * 1024 * 1024).round
           else 0
         val load_state = Load_State(Nil, rest, load_limit)