src/Pure/System/web_app.scala
changeset 80206 3cf3ad092e3e
parent 80205 fc2d791d28bd
child 80243 b2889dd54a2a
equal deleted inserted replaced
80205:fc2d791d28bd 80206:3cf3ad092e3e
   314       (if (serve_frontend) Path.explode("backend") else Path.current) +
   314       (if (serve_frontend) Path.explode("backend") else Path.current) +
   315         (if (external) api_base else Path.current) + path
   315         (if (external) api_base else Path.current) + path
   316 
   316 
   317     def route(path: Path, params: Properties.T = Nil): String = {
   317     def route(path: Path, params: Properties.T = Nil): String = {
   318       def param(p: Properties.Entry): String = Url.encode(p._1) + "=" + Url.encode(p._2)
   318       def param(p: Properties.Entry): String = Url.encode(p._1) + "=" + Url.encode(p._2)
   319       val route =
   319       if (params.isEmpty) path.implode else path.implode + "?" + params.map(param).mkString("&")
   320         if (params.isEmpty) path.implode else path.implode + "?" + params.map(param).mkString("&")
       
   321       "/" + route
       
   322     }
   320     }
   323 
   321 
   324     def api_route(path: Path, params: Properties.T = Nil, external: Boolean = true): String =
   322     def api_route(path: Path, params: Properties.T = Nil, external: Boolean = true): String =
   325       route(api_path(path, external = external), params)
   323       "/" + route(api_path(path, external = external), params)
   326 
   324 
   327     def frontend_url(path: Path, params: Properties.T = Nil): Url =
   325     def frontend_url(path: Path, params: Properties.T = Nil): Url =
   328       frontend.resolve(route(path, params))
   326       frontend.resolve(route(path, params))
   329   }
   327   }
   330 
   328